Higher modalities

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2023-03-09.
Last modified on 2023-06-28.

module orthogonal-factorization-systems.higher-modalities where

Imports

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.small-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.locally-small-modal-operators
open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.uniquely-eliminating-modalities

Idea

A higher modality is a higher mode of logic defined in terms of a monadic modal operator ○ satisfying a certain induction principle.

The induction principle states that for every type X and family P : ○ X → UU, to define a dependent map (x' : ○ X) → ○ (P x') it suffices to define it on the image of the modal unit, i.e. (x : X) → ○ (P (unit-○ x)). Moreover, it satisfies a computation principle stating that when evaluating a map defined in this manner on the image of the modal unit, one recovers the defining map (propositionally).

Lastly, higher modalities must also be identity closed in the sense that for every type X the identity types (x' ＝ y') are modal for all terms x' y' : ○ X. In other words, ○ X is ○-separated. Because of this, higher modalities in their most general form only make sense for locally small modal operators.

Definition

The universal property of higher modalities

module _
  {l1 l2 : Level}
  {○ : operator-modality l1 l2}
  (unit-○ : unit-modality ○)
  where

  ind-modality : UU (lsuc l1 ⊔ l2)
  ind-modality =
    (X : UU l1) (P : ○ X → UU l1) →
    ((x : X) → ○ (P (unit-○ x))) →
    (x' : ○ X) → ○ (P x')

  rec-modality : UU (lsuc l1 ⊔ l2)
  rec-modality = (X Y : UU l1) → (X → ○ Y) → ○ X → ○ Y

  compute-ind-modality : ind-modality → UU (lsuc l1 ⊔ l2)
  compute-ind-modality ind-○ =
    (X : UU l1) (P : ○ X → UU l1) →
    (f : (x : X) → ○ (P (unit-○ x))) →
    (x : X) → ind-○ X P f (unit-○ x) ＝ f x

  dependent-universal-property-modality : UU (lsuc l1 ⊔ l2)
  dependent-universal-property-modality =
    Σ ind-modality compute-ind-modality

  rec-modality-ind-modality : ind-modality → rec-modality
  rec-modality-ind-modality ind X Y = ind X (λ _ → Y)

Closure under identity type formers

We say that the locally small type of a locally small type are modal if their small equivalent is modal. We say that a modality is closed under identity type formation if, for every modal type, their identity types are also modal.

module _
  {l1 l2 : Level}
  ((○ , is-locally-small-○) : locally-small-operator-modality l1 l2 l1)
  (unit-○ : unit-modality ○)
  where

  is-modal-identity-types : UU (lsuc l1 ⊔ l2)
  is-modal-identity-types =
    (X : UU l1) (x y : ○ X) →
    is-modal-type-is-small (unit-○) (x ＝ y) (is-locally-small-○ X x y)

The `is-higher-modality` predicate

  is-higher-modality : UU (lsuc l1 ⊔ l2)
  is-higher-modality =
    dependent-universal-property-modality (unit-○) × is-modal-identity-types

Components of a `is-higher-modality` proof

  ind-modality-is-higher-modality : is-higher-modality → ind-modality unit-○
  ind-modality-is-higher-modality = pr1 ∘ pr1

  rec-modality-is-higher-modality : is-higher-modality → rec-modality unit-○
  rec-modality-is-higher-modality =
    rec-modality-ind-modality unit-○ ∘ ind-modality-is-higher-modality

  compute-ind-modality-is-higher-modality :
    (h : is-higher-modality) →
    compute-ind-modality unit-○ (ind-modality-is-higher-modality h)
  compute-ind-modality-is-higher-modality = pr2 ∘ pr1

  is-modal-identity-types-is-higher-modality :
    is-higher-modality → is-modal-identity-types
  is-modal-identity-types-is-higher-modality = pr2

The structure of a higher modality

higher-modality : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
higher-modality l1 l2 =
  Σ ( locally-small-operator-modality l1 l2 l1)
    ( λ ○ →
      Σ ( unit-modality (pr1 ○))
        ( is-higher-modality ○))

Compoents of a higher modality

module _
  {l1 l2 : Level} (h : higher-modality l1 l2)
  where

  locally-small-operator-higher-modality :
    locally-small-operator-modality l1 l2 l1
  locally-small-operator-higher-modality = pr1 h

  operator-higher-modality : operator-modality l1 l2
  operator-higher-modality =
    operator-modality-locally-small-operator-modality
      ( locally-small-operator-higher-modality)

  is-locally-small-operator-higher-modality :
    is-locally-small-operator-modality l1 (operator-higher-modality)
  is-locally-small-operator-higher-modality =
    is-locally-small-locally-small-operator-modality
      ( locally-small-operator-higher-modality)

  unit-higher-modality :
    unit-modality (operator-higher-modality)
  unit-higher-modality = pr1 (pr2 h)

  is-higher-modality-higher-modality :
    is-higher-modality
      ( locally-small-operator-higher-modality)
      ( unit-higher-modality)
  is-higher-modality-higher-modality = pr2 (pr2 h)

  ind-modality-higher-modality :
    ind-modality (unit-higher-modality)
  ind-modality-higher-modality =
    ind-modality-is-higher-modality
      ( locally-small-operator-higher-modality)
      ( unit-higher-modality)
      ( is-higher-modality-higher-modality)

  rec-modality-higher-modality :
    rec-modality (unit-higher-modality)
  rec-modality-higher-modality =
    rec-modality-ind-modality
      ( unit-higher-modality)
      ( ind-modality-higher-modality)

  compute-ind-modality-higher-modality :
    compute-ind-modality
      ( unit-higher-modality)
      ( ind-modality-higher-modality)
  compute-ind-modality-higher-modality =
    compute-ind-modality-is-higher-modality
      ( locally-small-operator-higher-modality)
      ( unit-higher-modality)
      ( is-higher-modality-higher-modality)

  is-modal-identity-types-higher-modality :
    is-modal-identity-types
      ( locally-small-operator-higher-modality)
      ( unit-higher-modality)
  is-modal-identity-types-higher-modality =
    ( is-modal-identity-types-is-higher-modality)
    ( locally-small-operator-higher-modality)
    ( unit-higher-modality)
    ( is-higher-modality-higher-modality)

Properties

module _
  {l : Level}
  {○ : operator-modality l l} (unit-○ : unit-modality ○)
  where

  map-rec-modality :
    (rec-○ : rec-modality unit-○) {X Y : UU l} → (X → Y) → ○ X → ○ Y
  map-rec-modality rec-○ {X} {Y} f = rec-○ X Y (unit-○ ∘ f)

module _
  {l1 l2 : Level}
  ((○ , is-locally-small-○) : locally-small-operator-modality l1 l2 l1)
  (unit-○ : unit-modality ○)
  (Id-○ : is-modal-identity-types (○ , is-locally-small-○) unit-○)
  where

  elim-Id-higher-modality :
    {X : UU l1} {x' y' : ○ X} →
    ○ (type-is-small (is-locally-small-○ X x' y')) → x' ＝ y'
  elim-Id-higher-modality {X} {x'} {y'} =
    map-inv-unit-is-modal-type-is-small unit-○
      ( x' ＝ y')
      ( is-locally-small-○ X x' y')
      ( Id-○ X x' y')

module _
  {l : Level}
  ( ((○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) :
      higher-modality l l)
  where

  map-inv-unit-id-higher-modality :
    {X : UU l} {x' y' : ○ X} → ○ (x' ＝ y') → x' ＝ y'
  map-inv-unit-id-higher-modality {X} {x'} {y'} =
    map-inv-unit-is-modal-type-is-small unit-○
      ( x' ＝ y')
      ( is-locally-small-○ X x' y')
      ( Id-○ X x' y') ∘
      ( map-rec-modality unit-○
        ( rec-modality-ind-modality unit-○ ind-○)
        ( map-equiv-is-small ( is-locally-small-○ X x' y')))

module _
  {l : Level}
  ( ((○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) :
      higher-modality l l)
  (X : UU l)
  where

  map-inv-unit-higher-modality : ○ (○ X) → ○ X
  map-inv-unit-higher-modality = ind-○ (○ X) (λ _ → X) id

  is-retraction-map-inv-unit-higher-modality :
    (map-inv-unit-higher-modality ∘ unit-○) ~ id
  is-retraction-map-inv-unit-higher-modality = compute-ind-○ (○ X) (λ _ → X) id

  is-section-map-inv-unit-higher-modality :
    (unit-○ ∘ map-inv-unit-higher-modality) ~ id
  is-section-map-inv-unit-higher-modality x'' =
    map-inv-unit-id-higher-modality
      ( (○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○)
      ( ind-○ (○ X)
        ( λ x'' → unit-○ (map-inv-unit-higher-modality x'') ＝ x'')
        ( unit-○ ∘ (ap unit-○ ∘ is-retraction-map-inv-unit-higher-modality))
        ( x''))

  is-modal-operator-modality-type : is-modal unit-○ (○ X)
  pr1 (pr1 is-modal-operator-modality-type) = map-inv-unit-higher-modality
  pr2 (pr1 is-modal-operator-modality-type) =
    is-section-map-inv-unit-higher-modality
  pr1 (pr2 is-modal-operator-modality-type) = map-inv-unit-higher-modality
  pr2 (pr2 is-modal-operator-modality-type) =
    is-retraction-map-inv-unit-higher-modality