Double negation sheaves

Content created by Fredrik Bakke.

Created on 2024-10-15.
Last modified on 2024-10-15.

module orthogonal-factorization-systems.double-negation-sheaves where
Imports 
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.double-negation-stable-propositions
open import foundation.empty-types
open import foundation.irrefutable-propositions
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.universal-property-coproduct-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions

open import orthogonal-factorization-systems.null-types

Idea

Double negation sheaves are types that are null at irrefutable propositions, i.e., propositions P for which the double negation ¬¬P is true.

Double negation sheaves were first introduced in the context of Homotopy Type Theory in Example 3.41 of [RSS20], and are considered in the restricted context of sets in [Swa24].

Definitions

The property of being a double negation sheaf

is-double-negation-sheaf :
  (l1 : Level) {l2 : Level} (A : UU l2) → UU (lsuc l1 ⊔ l2)
is-double-negation-sheaf l1 A =
  (P : Irrefutable-Prop l1) → is-null (type-Irrefutable-Prop P) A

is-prop-is-double-negation-sheaf :
  {l1 l2 : Level} {A : UU l2} → is-prop (is-double-negation-sheaf l1 A)
is-prop-is-double-negation-sheaf {A = A} =
  is-prop-Π (λ P → is-prop-is-null (type-Irrefutable-Prop P) A)

Properties

The empty type is a double negation sheaf

is-double-negation-sheaf-empty :
  {l : Level} → is-double-negation-sheaf l empty
is-double-negation-sheaf-empty P =
  is-equiv-has-converse empty-Prop
    ( hom-Prop (prop-Irrefutable-Prop P) empty-Prop)
    ( is-irrefutable-Irrefutable-Prop P)

Contractible types are double negation sheaves

is-double-negation-sheaf-is-contr :
  {l1 l2 : Level} {A : UU l1} → is-contr A → is-double-negation-sheaf l2 A
is-double-negation-sheaf-is-contr is-contr-A P =
  is-null-is-contr (type-Irrefutable-Prop P) is-contr-A

Propositions that are double negation sheaves are double negation stable

module _
  {l : Level} {A : UU l}
  (is-prop-A : is-prop A)
  (is-¬¬sheaf-A : is-double-negation-sheaf l A)
  where

  compute-is-double-negation-sheaf-is-prop : A ≃ (¬ A → A)
  compute-is-double-negation-sheaf-is-prop =
    ( left-unit-law-product-is-contr
      ( is-proof-irrelevant-is-prop (is-prop-function-type is-prop-A) id)) ∘e
    ( equiv-universal-property-coproduct A) ∘e
    ( _ , is-¬¬sheaf-A (is-decidable-prop-Irrefutable-Prop (A , is-prop-A)))

  is-double-negation-stable-is-double-negation-sheaf-is-prop :
    is-double-negation-stable (A , is-prop-A)
  is-double-negation-stable-is-double-negation-sheaf-is-prop ¬¬a =
    map-inv-is-equiv (is-¬¬sheaf-A (A , is-prop-A , ¬¬a)) id

Double negation stable propositions are double negation sheaves

This follows from the fact that a proposition P is double negation stable if and only if it is local at all double negations

  (¬¬A → P) → (A → P),

and nullification at irrefutable propositions is a restriction of this.

This remains to be formalized.

The negation of a type is a double negation sheaf

This is a corollary of the previous result.

This remains to be formalized.

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.
[Swa24]
Andrew W Swan. Oracle modalities. 2024. arXiv:2406.05818.

Recent changes