Higher modalities
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2023-03-09.
Last modified on 2024-03-12.
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.precomposition-dependent-functions open import foundation.retractions open import foundation.small-types open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels open import orthogonal-factorization-systems.locally-small-modal-operators open import orthogonal-factorization-systems.modal-induction open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.modal-subuniverse-induction 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
Closure under identity type formers
We say that the identity types 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-small-identity-types : UU (lsuc l1 ⊔ l2) is-modal-small-identity-types = (X : UU l1) (x y : ○ X) → is-modal-type-is-small (unit-○) (x = y) (is-locally-small-○ X x y)
The predicate of being a higher modality
is-higher-modality : UU (lsuc l1 ⊔ l2) is-higher-modality = induction-principle-modality (unit-○) × is-modal-small-identity-types
Components of a higher modality proof
module _ {l1 l2 : Level} (locally-small-○ : locally-small-operator-modality l1 l2 l1) (unit-○ : unit-modality (pr1 locally-small-○)) (h : is-higher-modality locally-small-○ unit-○) where induction-principle-is-higher-modality : induction-principle-modality unit-○ induction-principle-is-higher-modality = pr1 h ind-is-higher-modality : ind-modality unit-○ ind-is-higher-modality = ind-induction-principle-modality ( unit-○) ( induction-principle-is-higher-modality) compute-ind-is-higher-modality : compute-ind-modality unit-○ ind-is-higher-modality compute-ind-is-higher-modality = compute-ind-induction-principle-modality ( unit-○) ( induction-principle-is-higher-modality) recursion-principle-is-higher-modality : recursion-principle-modality unit-○ recursion-principle-is-higher-modality = recursion-principle-induction-principle-modality ( unit-○) ( induction-principle-is-higher-modality) rec-is-higher-modality : rec-modality unit-○ rec-is-higher-modality = rec-recursion-principle-modality ( unit-○) ( recursion-principle-is-higher-modality) compute-rec-is-higher-modality : compute-rec-modality unit-○ rec-is-higher-modality compute-rec-is-higher-modality = compute-rec-recursion-principle-modality ( unit-○) ( recursion-principle-is-higher-modality) is-modal-small-identity-types-is-higher-modality : is-modal-small-identity-types locally-small-○ unit-○ is-modal-small-identity-types-is-higher-modality = pr2 h
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 ○))
Components 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) induction-principle-higher-modality : induction-principle-modality (unit-higher-modality) induction-principle-higher-modality = induction-principle-is-higher-modality ( locally-small-operator-higher-modality) ( unit-higher-modality) ( is-higher-modality-higher-modality) ind-higher-modality : ind-modality (unit-higher-modality) ind-higher-modality = ind-induction-principle-modality ( unit-higher-modality) ( induction-principle-higher-modality) compute-ind-higher-modality : compute-ind-modality ( unit-higher-modality) ( ind-higher-modality) compute-ind-higher-modality = compute-ind-induction-principle-modality ( unit-higher-modality) ( induction-principle-higher-modality) recursion-principle-higher-modality : recursion-principle-modality (unit-higher-modality) recursion-principle-higher-modality = recursion-principle-is-higher-modality ( locally-small-operator-higher-modality) ( unit-higher-modality) ( is-higher-modality-higher-modality) rec-higher-modality : rec-modality (unit-higher-modality) rec-higher-modality = rec-recursion-principle-modality ( unit-higher-modality) ( recursion-principle-higher-modality) compute-rec-higher-modality : compute-rec-modality (unit-higher-modality) (rec-higher-modality) compute-rec-higher-modality = compute-rec-recursion-principle-modality ( unit-higher-modality) ( recursion-principle-higher-modality) is-modal-small-identity-type-higher-modality : is-modal-small-identity-types ( locally-small-operator-higher-modality) ( unit-higher-modality) is-modal-small-identity-type-higher-modality = ( is-modal-small-identity-types-is-higher-modality) ( locally-small-operator-higher-modality) ( unit-higher-modality) ( is-higher-modality-higher-modality)
Properties
Subuniverse induction for higher modalities
module _ {l1 l2 : Level} (m : higher-modality l1 l2) where strong-ind-subuniverse-higher-modality : strong-ind-subuniverse-modality (unit-higher-modality m) strong-ind-subuniverse-higher-modality = strong-ind-subuniverse-ind-modality ( unit-higher-modality m) ( ind-higher-modality m) compute-strong-ind-subuniverse-higher-modality : compute-strong-ind-subuniverse-modality ( unit-higher-modality m) ( strong-ind-subuniverse-higher-modality) compute-strong-ind-subuniverse-higher-modality = compute-strong-ind-subuniverse-ind-modality ( unit-higher-modality m) ( ind-higher-modality m) ( compute-ind-higher-modality m) ind-subuniverse-higher-modality : ind-subuniverse-modality (unit-higher-modality m) ind-subuniverse-higher-modality = ind-subuniverse-ind-modality ( unit-higher-modality m) ( ind-higher-modality m) compute-ind-subuniverse-higher-modality : compute-ind-subuniverse-modality ( unit-higher-modality m) ( ind-subuniverse-higher-modality) compute-ind-subuniverse-higher-modality = compute-ind-subuniverse-ind-modality ( unit-higher-modality m) ( ind-higher-modality m) ( compute-ind-higher-modality m) strong-rec-subuniverse-higher-modality : strong-rec-subuniverse-modality (unit-higher-modality m) strong-rec-subuniverse-higher-modality = strong-rec-subuniverse-rec-modality ( unit-higher-modality m) ( rec-higher-modality m) compute-strong-rec-subuniverse-higher-modality : compute-strong-rec-subuniverse-modality ( unit-higher-modality m) ( strong-rec-subuniverse-higher-modality) compute-strong-rec-subuniverse-higher-modality = compute-strong-rec-subuniverse-rec-modality ( unit-higher-modality m) ( rec-higher-modality m) ( compute-rec-higher-modality m) rec-subuniverse-higher-modality : rec-subuniverse-modality (unit-higher-modality m) rec-subuniverse-higher-modality = rec-subuniverse-rec-modality ( unit-higher-modality m) ( rec-higher-modality m) compute-rec-subuniverse-higher-modality : compute-rec-subuniverse-modality ( unit-higher-modality m) ( rec-subuniverse-higher-modality) compute-rec-subuniverse-higher-modality = compute-rec-subuniverse-rec-modality ( unit-higher-modality m) ( rec-higher-modality m) ( compute-rec-higher-modality m)
When l1 = l2
, the identity types are modal in the usual sense
map-inv-unit-small-Id-higher-modality : {l1 l2 : Level} (m : higher-modality l1 l2) {X : UU l1} {x' y' : operator-higher-modality m X} → ( operator-higher-modality m ( type-is-small (is-locally-small-operator-higher-modality m X x' y'))) → x' = y' map-inv-unit-small-Id-higher-modality m {X} {x'} {y'} = map-inv-unit-is-modal-type-is-small ( unit-higher-modality m) ( x' = y') ( is-locally-small-operator-higher-modality m X x' y') ( is-modal-small-identity-type-higher-modality m X x' y') module _ {l : Level} (m : higher-modality l l) where map-inv-unit-Id-higher-modality : {X : UU l} {x' y' : operator-higher-modality m X} → operator-higher-modality m (x' = y') → x' = y' map-inv-unit-Id-higher-modality {X} {x'} {y'} = map-inv-unit-small-Id-higher-modality m ∘ ( ap-map-ind-modality ( unit-higher-modality m) ( ind-higher-modality m) ( map-equiv-is-small ( is-locally-small-operator-higher-modality m X x' y'))) is-section-unit-Id-higher-modality : {X : UU l} {x' y' : operator-higher-modality m X} → (map-inv-unit-Id-higher-modality ∘ unit-higher-modality m {x' = y'}) ~ id is-section-unit-Id-higher-modality {X} {x'} {y'} p = ( ap ( map-inv-equiv ( equiv-unit-is-modal-type-is-small ( unit-higher-modality m) ( x' = y') ( is-small-x'=y') ( is-modal-small-x'=y'))) ( compute-rec-higher-modality m ( unit-higher-modality m ∘ map-equiv-is-small is-small-x'=y') ( p))) ∙ ( htpy-eq ( distributive-map-inv-comp-equiv ( equiv-is-small is-small-x'=y') ( unit-higher-modality m , is-modal-small-x'=y')) ( unit-higher-modality m (map-equiv-is-small is-small-x'=y' p))) ∙ ( ap ( map-inv-equiv-is-small is-small-x'=y') ( is-retraction-map-inv-is-equiv is-modal-small-x'=y' ( map-equiv-is-small is-small-x'=y' p))) ∙ ( is-retraction-map-inv-equiv (equiv-is-small is-small-x'=y') p) where is-small-x'=y' = is-locally-small-operator-higher-modality m X x' y' is-modal-small-x'=y' = is-modal-small-identity-type-higher-modality m X x' y' retraction-unit-Id-higher-modality : {X : UU l} {x' y' : operator-higher-modality m X} → retraction (unit-higher-modality m {x' = y'}) pr1 retraction-unit-Id-higher-modality = map-inv-unit-Id-higher-modality pr2 retraction-unit-Id-higher-modality = is-section-unit-Id-higher-modality
We get this retraction without applying univalence, so, using strong subuniverse induction we can generally avoid it. However, we appeal to univalence to get the full equivalence.
is-modal-Id-higher-modality : {X : UU l} {x' y' : operator-higher-modality m X} → is-modal (unit-higher-modality m) (x' = y') is-modal-Id-higher-modality {X} {x'} {y'} = tr ( is-modal (unit-higher-modality m)) ( eq-equiv ( inv-equiv-is-small ( is-locally-small-operator-higher-modality m X x' y'))) ( is-modal-small-identity-type-higher-modality m X x' y')
Subuniverse induction on identity types
module _ {l : Level} (m : higher-modality l l) where ind-subuniverse-Id-higher-modality : {X : UU l} {Y : operator-higher-modality m X → UU l} (f g : (x' : operator-higher-modality m X) → operator-higher-modality m (Y x')) → (f ∘ unit-higher-modality m) ~ (g ∘ unit-higher-modality m) → f ~ g ind-subuniverse-Id-higher-modality {X} f g = strong-ind-subuniverse-higher-modality m ( λ x' → f x' = g x') ( λ _ → retraction-unit-Id-higher-modality m) compute-ind-subuniverse-Id-higher-modality : {X : UU l} {Y : operator-higher-modality m X → UU l} (f g : (x' : operator-higher-modality m X) → operator-higher-modality m (Y x')) → (H : (f ∘ unit-higher-modality m) ~ (g ∘ unit-higher-modality m)) → (x : X) → ( strong-ind-subuniverse-higher-modality m ( λ x' → f x' = g x') ( λ _ → retraction-unit-Id-higher-modality m) ( H) ( unit-higher-modality m x)) = ( H x) compute-ind-subuniverse-Id-higher-modality f g = compute-strong-ind-subuniverse-higher-modality m ( λ x → f x = g x) ( λ _ → retraction-unit-Id-higher-modality m)
Types in the image of the modal operator are modal
module _ {l : Level} (m : higher-modality l l) (X : UU l) where map-inv-unit-higher-modality : operator-higher-modality m (operator-higher-modality m X) → operator-higher-modality m X map-inv-unit-higher-modality = rec-higher-modality m id is-retraction-map-inv-unit-higher-modality : map-inv-unit-higher-modality ∘ unit-higher-modality m ~ id is-retraction-map-inv-unit-higher-modality = compute-rec-higher-modality m id is-section-map-inv-unit-higher-modality : unit-higher-modality m ∘ map-inv-unit-higher-modality ~ id is-section-map-inv-unit-higher-modality = ind-subuniverse-Id-higher-modality m _ _ ( ap (unit-higher-modality m) ∘ is-retraction-map-inv-unit-higher-modality) is-modal-operator-type-higher-modality : is-modal (unit-higher-modality m) (operator-higher-modality m X) pr1 (pr1 is-modal-operator-type-higher-modality) = map-inv-unit-higher-modality pr2 (pr1 is-modal-operator-type-higher-modality) = is-section-map-inv-unit-higher-modality pr1 (pr2 is-modal-operator-type-higher-modality) = map-inv-unit-higher-modality pr2 (pr2 is-modal-operator-type-higher-modality) = is-retraction-map-inv-unit-higher-modality
Higher modalities are uniquely eliminating modalities
is-section-ind-higher-modality : {l1 l2 : Level} (m : higher-modality l1 l2) {X : UU l1} {P : operator-higher-modality m X → UU l1} → ( ( precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P)) ∘ ( ind-higher-modality m P)) ~ ( id) is-section-ind-higher-modality m = is-section-ind-modality ( unit-higher-modality m) ( ind-higher-modality m) ( compute-ind-higher-modality m) module _ {l : Level} (m : higher-modality l l) where is-retraction-ind-higher-modality : {X : UU l} (P : operator-higher-modality m X → UU l) → ( ind-higher-modality m P ∘ precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P)) ~ ( id) is-retraction-ind-higher-modality P s = eq-htpy ( ind-subuniverse-Id-higher-modality m _ _ ( compute-ind-higher-modality m P (s ∘ unit-higher-modality m))) is-equiv-ind-higher-modality : {X : UU l} (P : operator-higher-modality m X → UU l) → is-equiv (ind-higher-modality m P) pr1 (pr1 (is-equiv-ind-higher-modality P)) = precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P) pr2 (pr1 (is-equiv-ind-higher-modality P)) = is-retraction-ind-higher-modality P pr1 (pr2 (is-equiv-ind-higher-modality P)) = precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P) pr2 (pr2 (is-equiv-ind-higher-modality P)) = is-section-ind-higher-modality m equiv-ind-higher-modality : {X : UU l} (P : operator-higher-modality m X → UU l) → ((x : X) → operator-higher-modality m (P (unit-higher-modality m x))) ≃ ((x' : operator-higher-modality m X) → operator-higher-modality m (P x')) pr1 (equiv-ind-higher-modality P) = ind-higher-modality m P pr2 (equiv-ind-higher-modality P) = is-equiv-ind-higher-modality P is-uniquely-eliminating-higher-modality : is-uniquely-eliminating-modality (unit-higher-modality m) is-uniquely-eliminating-higher-modality P = is-equiv-map-inv-is-equiv (is-equiv-ind-higher-modality P)
See also
The equivalent notions of
- Uniquely eliminating modalities
- Σ-closed reflective modalities
- Σ-closed reflective subuniverses
- Stable orthogonal factorization systems
References
- [RSS20]
- Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 01 2020. URL: https://lmcs.episciences.org/6015, arXiv:1706.07526, doi:10.23638/LMCS-16(1:2)2020.
Recent changes
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2024-02-27. Fredrik Bakke. A small optimization to equivalence relations (#1040).
- 2024-02-07. Fredrik Bakke. Deduplicate definitions (#1022).
- 2024-01-12. Fredrik Bakke. Make type arguments implicit for
eq-equiv
(#998). - 2023-11-24. Egbert Rijke. Refactor precomposition (#937).