The double negation modality
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-06-08.
Last modified on 2024-04-11.
module foundation.double-negation-modality where
Imports
open import foundation.double-negation open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.propositions open import foundation-core.transport-along-identifications open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.uniquely-eliminating-modalities
Idea
The double negation operation ¬¬
is a
modality.
Definition
The double negation modality
operator-double-negation-modality : (l : Level) → operator-modality l l operator-double-negation-modality _ = ¬¬_ unit-double-negation-modality : {l : Level} → unit-modality (operator-double-negation-modality l) unit-double-negation-modality = intro-double-negation
Properties
The double negation modality is a uniquely eliminating modality
is-uniquely-eliminating-modality-double-negation-modality : {l : Level} → is-uniquely-eliminating-modality (unit-double-negation-modality {l}) is-uniquely-eliminating-modality-double-negation-modality {l} {A} P = is-local-dependent-type-is-prop ( unit-double-negation-modality) ( operator-double-negation-modality l ∘ P) ( λ _ → is-prop-double-negation) ( λ f z → double-negation-extend ( λ (a : A) → tr ( ¬¬_ ∘ P) ( eq-is-prop is-prop-double-negation) ( f a)) ( z))
This proof follows Example 1.9 in [RSS20].
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-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2024-01-14. Fredrik Bakke. Exponentiating retracts of maps (#989).
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).
- 2023-11-01. Fredrik Bakke. Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions (#880).