From df14f7e0405fc02839c87192b7e76bafdd19daa8 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 15 Oct 2024 22:53:01 +0200
Subject: [PATCH] Define double negation sheaves (#1198)

---
 references.bib                                |  10 ++
 scripts/utils/__init__.py                     |  15 ++-
 src/foundation.lagda.md                       |   2 +
 src/foundation/decidable-types.lagda.md       |  14 +-
 ...uble-negation-stable-propositions.lagda.md |  83 ++++++++++++
 .../irrefutable-propositions.lagda.md         | 126 ++++++++++++++++++
 .../law-of-excluded-middle.lagda.md           |   3 +
 src/orthogonal-factorization-systems.lagda.md |   1 +
 .../double-negation-sheaves.lagda.md          | 123 +++++++++++++++++
 .../null-types.lagda.md                       |  11 ++
 10 files changed, 377 insertions(+), 11 deletions(-)
 create mode 100644 src/foundation/double-negation-stable-propositions.lagda.md
 create mode 100644 src/foundation/irrefutable-propositions.lagda.md
 create mode 100644 src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md

diff --git a/references.bib b/references.bib
index c187b5558f..8e6c24919d 100644
--- a/references.bib
+++ b/references.bib
@@ -690,6 +690,16 @@ @inproceedings{SvDR20
   keywords  = {higher inductive types,homotopy type theory,sequential colimits}
 }
 
+@misc{Swan24,
+  title         = {Oracle modalities},
+  author        = {Swan, Andrew W},
+  year          = {2024},
+  eprint        = {2406.05818},
+  archiveprefix = {arXiv},
+  eprintclass   = {math},
+  primaryclass  = {math.LO}
+}
+
 @book{SymmetryBook,
   title     = {Symmetry},
   author    = {Bezem, Marc and Buchholtz, Ulrik and Cagne, Pierre and Dundas, Bjørn Ian and Grayson, Daniel R},
diff --git a/scripts/utils/__init__.py b/scripts/utils/__init__.py
index d2afbd59b4..3bbae74c5d 100644
--- a/scripts/utils/__init__.py
+++ b/scripts/utils/__init__.py
@@ -219,14 +219,21 @@ def get_git_tracked_files():
     git_tracked_files = map(pathlib.Path, git_output.strip().split('\n'))
     return git_tracked_files
 
-
 def get_git_last_modified(file_path):
     try:
         # Get the last commit date for the file
-        output = subprocess.check_output(['git', 'log', '-1', '--format=%at', file_path], stderr=subprocess.DEVNULL)
-        return int(output.strip())
+        output = subprocess.check_output(
+            ['git', 'log', '-1', '--format=%at', file_path],
+            stderr=subprocess.DEVNULL
+        )
+        output_str = output.strip()
+        if output_str:
+            return int(output_str)
+        else:
+            # Output is empty, file may be untracked
+            return os.path.getmtime(file_path)
     except subprocess.CalledProcessError:
-        # If the file is not in git or there's an error, return last modified time according to OS
+        # If the git command fails, fall back to filesystem modification time
         return os.path.getmtime(file_path)
 
 def is_file_modified(file_path):
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 83228240ab..9d2c66f3a9 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -136,6 +136,7 @@ open import foundation.disjunction public
 open import foundation.double-arrows public
 open import foundation.double-negation public
 open import foundation.double-negation-modality public
+open import foundation.double-negation-stable-propositions public
 open import foundation.double-powersets public
 open import foundation.dubuc-penon-compact-types public
 open import foundation.effective-maps-equivalence-relations public
@@ -228,6 +229,7 @@ open import foundation.intersections-subtypes public
 open import foundation.inverse-sequential-diagrams public
 open import foundation.invertible-maps public
 open import foundation.involutions public
+open import foundation.irrefutable-propositions public
 open import foundation.isolated-elements public
 open import foundation.isomorphisms-of-sets public
 open import foundation.iterated-cartesian-product-types public
diff --git a/src/foundation/decidable-types.lagda.md b/src/foundation/decidable-types.lagda.md
index 3cfb7b915a..2f34bdc31f 100644
--- a/src/foundation/decidable-types.lagda.md
+++ b/src/foundation/decidable-types.lagda.md
@@ -245,13 +245,8 @@ double-negation-elim-is-decidable (inl x) p = x
 double-negation-elim-is-decidable (inr x) p = ex-falso (p x)
 ```
 
-### The double negation of `is-decidable` is always provable
-
-```agda
-double-negation-is-decidable : {l : Level} {P : UU l} → ¬¬ (is-decidable P)
-double-negation-is-decidable {P = P} f =
-  map-neg (inr {A = P} {B = ¬ P}) f (map-neg (inl {A = P} {B = ¬ P}) f)
-```
+See also
+[double negation stable propositions](foundation.double-negation-stable-propositions.md).
 
 ### Decidable types have ε-operators
 
@@ -354,3 +349,8 @@ module _
     ( is-inhabited-or-empty-is-merely-decidable ,
       is-merely-decidable-is-inhabited-or-empty)
 ```
+
+## See also
+
+- That decidablity is irrefutable is shown in
+  [`foundation.irrefutable-propositions`](foundation.irrefutable-propositions.md).
diff --git a/src/foundation/double-negation-stable-propositions.lagda.md b/src/foundation/double-negation-stable-propositions.lagda.md
new file mode 100644
index 0000000000..760c158524
--- /dev/null
+++ b/src/foundation/double-negation-stable-propositions.lagda.md
@@ -0,0 +1,83 @@
+# Double negation stable propositions
+
+```agda
+module foundation.double-negation-stable-propositions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.double-negation
+open import foundation.empty-types
+open import foundation.negation
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+A [proposition](foundation-core.propositions.md) `P` is
+{{#concept "double negation stable" Disambiguation="proposition" Agda=is-double-negation-stable}}
+if the implication
+
+```text
+  ¬¬P ⇒ P
+```
+
+is true. In other words, if [double negation](foundation.double-negation.md)
+elimination is valid for `P`.
+
+## Definitions
+
+### The predicate on a proposition of being double negation stable
+
+```agda
+module _
+  {l : Level} (P : Prop l)
+  where
+
+  is-double-negation-stable-Prop : Prop l
+  is-double-negation-stable-Prop = ¬¬' P ⇒ P
+
+  is-double-negation-stable : UU l
+  is-double-negation-stable = type-Prop is-double-negation-stable-Prop
+
+  is-prop-is-double-negation-stable : is-prop is-double-negation-stable
+  is-prop-is-double-negation-stable =
+    is-prop-type-Prop is-double-negation-stable-Prop
+```
+
+## Properties
+
+### The empty proposition is double negation stable
+
+```agda
+is-double-negation-stable-empty : is-double-negation-stable empty-Prop
+is-double-negation-stable-empty e = e id
+```
+
+### The unit proposition is double negation stable
+
+```agda
+is-double-negation-stable-unit : is-double-negation-stable unit-Prop
+is-double-negation-stable-unit _ = star
+```
+
+### The negation of a type is double negation stable
+
+```agda
+is-double-negation-stable-neg :
+  {l : Level} (A : UU l) → is-double-negation-stable (neg-type-Prop A)
+is-double-negation-stable-neg = double-negation-elim-neg
+```
+
+## See also
+
+- [The double negation modality](foundation.double-negation-modality.md)
+- [Irrefutable propositions](foundation.irrefutable-propositions.md) are double
+  negation stable.
diff --git a/src/foundation/irrefutable-propositions.lagda.md b/src/foundation/irrefutable-propositions.lagda.md
new file mode 100644
index 0000000000..7e0dd013dc
--- /dev/null
+++ b/src/foundation/irrefutable-propositions.lagda.md
@@ -0,0 +1,126 @@
+# Irrefutable propositions
+
+```agda
+module foundation.irrefutable-propositions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.coproduct-types
+open import foundation.decidable-propositions
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.double-negation
+open import foundation.function-types
+open import foundation.negation
+open import foundation.subuniverses
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+The [subuniverse](foundation.subuniverses.md) of
+{{#concept "irrefutable propositions" Agda=Irrefutable-Prop}} consists of
+[propositions](foundation-core.propositions.md) `P` for which the
+[double negation](foundation.double-negation.md) `¬¬P` is true.
+
+## Definitions
+
+### The predicate on a proposition of being irrefutable
+
+```agda
+is-irrefutable : {l : Level} → Prop l → UU l
+is-irrefutable P = ¬¬ (type-Prop P)
+
+is-prop-is-irrefutable : {l : Level} (P : Prop l) → is-prop (is-irrefutable P)
+is-prop-is-irrefutable P = is-prop-double-negation
+
+is-irrefutable-Prop : {l : Level} → Prop l → Prop l
+is-irrefutable-Prop = double-negation-Prop
+```
+
+### The subuniverse of irrefutable propositions
+
+```agda
+subuniverse-Irrefutable-Prop : (l : Level) → subuniverse l l
+subuniverse-Irrefutable-Prop l A =
+  product-Prop (is-prop-Prop A) (double-negation-type-Prop A)
+
+Irrefutable-Prop : (l : Level) → UU (lsuc l)
+Irrefutable-Prop l =
+  type-subuniverse (subuniverse-Irrefutable-Prop l)
+
+make-Irrefutable-Prop :
+  {l : Level} (P : Prop l) → is-irrefutable P → Irrefutable-Prop l
+make-Irrefutable-Prop P is-irrefutable-P =
+  ( type-Prop P , is-prop-type-Prop P , is-irrefutable-P)
+
+module _
+  {l : Level} (P : Irrefutable-Prop l)
+  where
+
+  type-Irrefutable-Prop : UU l
+  type-Irrefutable-Prop = pr1 P
+
+  is-prop-type-Irrefutable-Prop : is-prop type-Irrefutable-Prop
+  is-prop-type-Irrefutable-Prop = pr1 (pr2 P)
+
+  prop-Irrefutable-Prop : Prop l
+  prop-Irrefutable-Prop = type-Irrefutable-Prop , is-prop-type-Irrefutable-Prop
+
+  is-irrefutable-Irrefutable-Prop : is-irrefutable prop-Irrefutable-Prop
+  is-irrefutable-Irrefutable-Prop = pr2 (pr2 P)
+```
+
+## Properties
+
+### If it is irrefutable that a proposition is irrefutable, then the proposition is irrefutable
+
+```agda
+module _
+  {l : Level} (P : Prop l)
+  where
+
+  is-irrefutable-is-irrefutable-is-irrefutable :
+    is-irrefutable (is-irrefutable-Prop P) → is-irrefutable P
+  is-irrefutable-is-irrefutable-is-irrefutable =
+    double-negation-elim-neg (¬ (type-Prop P))
+```
+
+### The decidability of a proposition is irrefutable
+
+```agda
+is-irrefutable-is-decidable : {l : Level} {A : UU l} → ¬¬ (is-decidable A)
+is-irrefutable-is-decidable H = H (inr (H ∘ inl))
+
+module _
+  {l : Level} (P : Prop l)
+  where
+
+  is-irrefutable-is-decidable-Prop : is-irrefutable (is-decidable-Prop P)
+  is-irrefutable-is-decidable-Prop = is-irrefutable-is-decidable
+
+  is-decidable-prop-Irrefutable-Prop : Irrefutable-Prop l
+  is-decidable-prop-Irrefutable-Prop =
+    make-Irrefutable-Prop (is-decidable-Prop P) is-irrefutable-is-decidable-Prop
+```
+
+### Provable propositions are irrefutable
+
+```agda
+module _
+  {l : Level} (P : Prop l)
+  where
+
+  is-irrefutable-is-inhabited : type-Prop P → is-irrefutable P
+  is-irrefutable-is-inhabited = intro-double-negation
+
+is-irrefutable-unit : is-irrefutable unit-Prop
+is-irrefutable-unit = is-irrefutable-is-inhabited unit-Prop star
+```
diff --git a/src/foundation/law-of-excluded-middle.lagda.md b/src/foundation/law-of-excluded-middle.lagda.md
index d82d58a594..3ee5bdb8c0 100644
--- a/src/foundation/law-of-excluded-middle.lagda.md
+++ b/src/foundation/law-of-excluded-middle.lagda.md
@@ -31,6 +31,9 @@ The {{#concept "law of excluded middle" Agda=LEM}} asserts that any
 ```agda
 LEM : (l : Level) → UU (lsuc l)
 LEM l = (P : Prop l) → is-decidable (type-Prop P)
+
+prop-LEM : (l : Level) → Prop (lsuc l)
+prop-LEM l = Π-Prop (Prop l) (is-decidable-Prop)
 ```
 
 ## Properties
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index 59412d4838..c1d6a104fe 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -13,6 +13,7 @@ open import orthogonal-factorization-systems.cd-structures public
 open import orthogonal-factorization-systems.cellular-maps public
 open import orthogonal-factorization-systems.closed-modalities public
 open import orthogonal-factorization-systems.double-lifts-families-of-elements public
+open import orthogonal-factorization-systems.double-negation-sheaves public
 open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public
 open import orthogonal-factorization-systems.extensions-of-maps public
diff --git a/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md b/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md
new file mode 100644
index 0000000000..eb2cbcdba9
--- /dev/null
+++ b/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md
@@ -0,0 +1,123 @@
+# Double negation sheaves
+
+```agda
+module orthogonal-factorization-systems.double-negation-sheaves where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+{{#concept "Double negation sheaves" Agda=is-double-negation-sheaf}} are types
+that are [null](orthogonal-factorization-systems.null-types.md) at
+[irrefutable propositions](foundation.irrefutable-propositions.md), i.e.,
+[propositions](foundation-core.propositions.md) `P` for which the
+[double negation](foundation.double-negation.md) `¬¬P` is true.
+
+Double negation sheaves were first introduced in the context of Homotopy Type
+Theory in Example 3.41 of {{#cite RSS20}}, and are considered in the restricted
+context of [sets](foundation-core.sets.md) in {{#cite Swan24}}.
+
+## Definitions
+
+### The property of being a double negation sheaf
+
+```agda
+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
+
+```agda
+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
+
+```agda
+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
+
+```agda
+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
+
+```text
+  (¬¬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
+
+{{#bibliography}}
diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md
index 6e50e36ba6..575cbff8c7 100644
--- a/src/orthogonal-factorization-systems/null-types.lagda.md
+++ b/src/orthogonal-factorization-systems/null-types.lagda.md
@@ -7,6 +7,7 @@ module orthogonal-factorization-systems.null-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.diagonal-maps-of-types
 open import foundation.equivalences
@@ -227,3 +228,13 @@ module _
     (A : UU l3) → ((x : X) → is-null (fiber f x) A) → is-local f A
   is-local-is-null-fiber A = is-local-dependent-type-is-null-fiber (λ _ → A)
 ```
+
+### Contractible types are null at all types
+
+```agda
+is-null-is-contr :
+  {l1 l2 : Level} {A : UU l1} (B : UU l2) → is-contr A → is-null B A
+is-null-is-contr {A = A} B is-contr-A =
+  is-null-is-local-terminal-map B A
+    ( is-local-is-contr (terminal-map B) A is-contr-A)
+```