This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The double negation modality

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.