The closed modalities
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-06-08.
Last modified on 2023-09-15.
module orthogonal-factorization-systems.closed-modalities where
Imports
open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.reflective-subuniverses open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses open import synthetic-homotopy-theory.joins-of-types
Idea
Given any proposition Q
, the
join operation _* Q
defines a
higher modality. We
call these the closed modalities.
Definition
operator-closed-modality : (l : Level) {lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ) operator-closed-modality l Q A = A * type-Prop Q unit-closed-modality : {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality l Q) unit-closed-modality Q {A} = inl-join A (type-Prop Q) is-closed-modal : {l lQ : Level} (Q : Prop lQ) → UU l → Prop (l ⊔ lQ) pr1 (is-closed-modal Q B) = type-Prop Q → is-contr B pr2 (is-closed-modal Q B) = is-prop-function-type is-property-is-contr
Properties
The closed modalities define Σ-closed reflective subuniverses
module _ {l lQ : Level} (Q : Prop lQ) where is-reflective-subuniverse-closed-modality : is-reflective-subuniverse {l ⊔ lQ} (is-closed-modal Q) pr1 is-reflective-subuniverse-closed-modality = operator-closed-modality (l ⊔ lQ) Q pr1 (pr2 is-reflective-subuniverse-closed-modality) = unit-closed-modality Q pr1 (pr2 (pr2 is-reflective-subuniverse-closed-modality)) A q = right-zero-law-join-is-contr ( A) ( type-Prop Q) ( is-proof-irrelevant-is-prop (is-prop-type-Prop Q) q) pr2 (pr2 (pr2 is-reflective-subuniverse-closed-modality)) B A is-modal-B = is-equiv-is-contr-map ( λ f → is-contr-equiv ( Σ (A → B) (_= f)) ( equiv-Σ ( _= f) ( right-unit-law-Σ-is-contr ( λ f' → is-contr-Σ ( is-contr-Π is-modal-B) ( center ∘ is-modal-B) ( is-contr-Π ( λ (a , q) → is-prop-is-contr ( is-modal-B q) ( f' a) ( center (is-modal-B q))))) ∘e ( equiv-up-join A (type-Prop Q) B)) ( λ _ → id-equiv)) ( is-contr-total-path' f)) reflective-subuniverse-closed-modality : reflective-subuniverse (l ⊔ lQ) (l ⊔ lQ) pr1 reflective-subuniverse-closed-modality = is-closed-modal Q pr2 reflective-subuniverse-closed-modality = is-reflective-subuniverse-closed-modality is-closed-under-Σ-reflective-subuniverse-closed-modality : is-closed-under-Σ-reflective-subuniverse ( reflective-subuniverse-closed-modality) is-closed-under-Σ-reflective-subuniverse-closed-modality A B q = is-contr-Σ ( pr2 A q) ( center (pr2 A q)) ( pr2 (B (center (pr2 A q))) q) closed-under-Σ-reflective-subuniverse-closed-modality : closed-under-Σ-reflective-subuniverse (l ⊔ lQ) (l ⊔ lQ) pr1 closed-under-Σ-reflective-subuniverse-closed-modality = reflective-subuniverse-closed-modality pr2 closed-under-Σ-reflective-subuniverse-closed-modality = is-closed-under-Σ-reflective-subuniverse-closed-modality
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-09-15. Egbert Rijke. update contributors, remove unused imports (#772).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).