Define double negation sheaves (#1198)

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},

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):

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

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).

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.

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
+```

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

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