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