The zero modality
Content created by Fredrik Bakke.
Created on 2023-06-08.
Last modified on 2023-11-24.
module orthogonal-factorization-systems.zero-modality where
Imports
open import foundation.unit-type open import foundation.universe-levels open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.uniquely-eliminating-modalities
Idea
The zero modality is the modality that maps every type to the unit type.
Definition
operator-zero-modality : (l1 l2 : Level) → operator-modality l1 l2 operator-zero-modality l1 l2 _ = raise-unit l2 unit-zero-modality : {l1 l2 : Level} → unit-modality (operator-zero-modality l1 l2) unit-zero-modality _ = raise-star
Properties
The zero modality is a uniquely eliminating modality
is-uniquely-eliminating-modality-zero-modality : {l1 l2 : Level} → is-uniquely-eliminating-modality (unit-zero-modality {l1} {l2}) is-uniquely-eliminating-modality-zero-modality {l2 = l2} P = is-local-is-contr ( unit-zero-modality) ( raise-unit l2) ( is-contr-raise-unit)
The zero modality is equivalent to -2
-truncation
This remains to be made formal. #739
Recent changes
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).
- 2023-09-10. Fredrik Bakke. Link issues to unfinished sections (#732).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).