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
The modal operator's action on maps
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)
Modal identity elimination
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')
For homogenous higher modalities, The identity types of modal types are modal in the usual sense
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')))
○ X
is modal
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
Higher modalities are uniquely eliminating modalities
module _ {l : Level} ( ((○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) : higher-modality l l) where is-retraction-ind-modality : {X : UU l} {P : ○ X → UU l} → (precomp-Π unit-○ (○ ∘ P) ∘ ind-○ X P) ~ id is-retraction-ind-modality {X} {P} = eq-htpy ∘ compute-ind-○ X P is-section-ind-modality : {X : UU l} {P : ○ X → UU l} → (ind-○ X P ∘ precomp-Π unit-○ (○ ∘ P)) ~ id is-section-ind-modality {X} {P} s = eq-htpy ( map-inv-unit-id-higher-modality ( (○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) ∘ ( ind-○ X ( λ x' → (ind-○ X P ∘ precomp-Π (unit-○) (○ ∘ P)) s x' = s x') ( unit-○ ∘ compute-ind-○ X P (s ∘ unit-○)))) is-equiv-ind-modality : (X : UU l) (P : ○ X → UU l) → is-equiv (ind-○ X P) pr1 (pr1 (is-equiv-ind-modality X P)) = precomp-Π unit-○ (○ ∘ P) pr2 (pr1 (is-equiv-ind-modality X P)) = is-section-ind-modality pr1 (pr2 (is-equiv-ind-modality X P)) = precomp-Π unit-○ (○ ∘ P) pr2 (pr2 (is-equiv-ind-modality X P)) = is-retraction-ind-modality equiv-ind-modality : (X : UU l) (P : ○ X → UU l) → ((x : X) → ○ (P (unit-○ x))) ≃ ((x' : ○ X) → ○ (P x')) pr1 (equiv-ind-modality X P) = ind-○ X P pr2 (equiv-ind-modality X P) = is-equiv-ind-modality X P is-uniquely-eliminating-modality-higher-modality : is-uniquely-eliminating-modality unit-○ is-uniquely-eliminating-modality-higher-modality X P = is-equiv-map-inv-is-equiv (is-equiv-ind-modality X P)
See also
The equivalent notions of
- Uniquely eliminating modalities
- Σ-closed reflective modalities
- Σ-closed reflective subuniverses
- Stable orthogonal factorization systems
References
- Egbert Rijke, Michael Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, Volume 16, Issue 1, 2020 (arXiv:1706.07526, doi:10.23638)
Recent changes
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-25. Fredrik Bakke. Fix alignment
where
blocks (#670). - 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).