The double negation modality
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-06-08.
Last modified on 2023-09-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
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 g → double-negation-extend ( λ (a : A) → tr ( ¬¬ ∘ P) ( eq-is-prop is-prop-double-negation) ( f a)) ( z) ( g))
This proof follows Example 1.9 in Modalities in homotopy type theory.
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-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 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).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).