From 3edcc3ac6d15fc847d1852b5bd83e6c43b7585bd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 29 Oct 2023 20:39:01 +0100
Subject: [PATCH 1/4] Moving closed notations at level 0 in anticipation of
 removing Coq's fallback ignoring levels when nothing else applies.

---
 Construction/Comma/Adjunction.v   |  2 +-
 Functor/Applicative.v             |  2 +-
 Functor/Diagonal.v                |  6 +++---
 Functor/Product/Internal.v        |  2 +-
 Functor/Structure/Monoidal/Pure.v |  2 +-
 Instance/Coq/Applicative.v        |  8 ++++----
 Theory/Coq/Applicative.v          | 10 +++++-----
 Theory/Coq/Functor.v              | 12 ++++++------
 Theory/Functor.v                  |  6 +++---
 9 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/Construction/Comma/Adjunction.v b/Construction/Comma/Adjunction.v
index d3299649..630a089f 100644
--- a/Construction/Comma/Adjunction.v
+++ b/Construction/Comma/Adjunction.v
@@ -56,7 +56,7 @@ Context {G : C ⟶ D}.
 Definition πD := comma_proj1.
 Definition πC := comma_proj2.
 
-#[local] Notation "⟨πD,πC⟩" := comma_proj (at level 100).
+#[local] Notation "⟨πD,πC⟩" := comma_proj (at level 0).
 
 Record lawvere_equiv := {
   lawvere_iso : F ↓ Id[C] ≅[Cat] Id[D] ↓ G;
diff --git a/Functor/Applicative.v b/Functor/Applicative.v
index cf0f2d21..bd7a85f1 100644
--- a/Functor/Applicative.v
+++ b/Functor/Applicative.v
@@ -36,4 +36,4 @@ Arguments Applicative {_ _} F.
 Arguments pure {C _ F _ _ _}.
 
 Notation "pure[ F ]" := (@pure _ _ F _ _ _)
-  (at level 9, format "pure[ F ]") : morphism_scope.
+  (at level 0, format "pure[ F ]") : morphism_scope.
diff --git a/Functor/Diagonal.v b/Functor/Diagonal.v
index a51127cf..7e2b0ccd 100644
--- a/Functor/Diagonal.v
+++ b/Functor/Diagonal.v
@@ -26,12 +26,12 @@ Program Instance Diagonal_Product `(C : Category) : C ⟶ C ∏ C.
 
 End Diagonal_Product.
 
-Notation "Δ[ J ]( c )" := (Diagonal J c) (at level 90, format "Δ[ J ]( c )") : functor_scope.
+Notation "Δ[ J ]( c )" := (Diagonal J c) (at level 0, format "Δ[ J ]( c )") : functor_scope.
 
 Require Import Category.Instance.One.
 
-Notation "Δ( c )" := (Diagonal _ c) (at level 90, format "Δ( c )") : functor_scope.
-Notation "=( c )" := (Diagonal 1 c) (at level 90, format "=( c )") : functor_scope.
+Notation "Δ( c )" := (Diagonal _ c) (at level 0, format "Δ( c )") : functor_scope.
+Notation "=( c )" := (Diagonal 1 c) (at level 0, format "=( c )") : functor_scope.
 
 Definition Δ {C J : Category} := @Diagonal C J.
 
diff --git a/Functor/Product/Internal.v b/Functor/Product/Internal.v
index fe5ec29c..2ce47d41 100644
--- a/Functor/Product/Internal.v
+++ b/Functor/Product/Internal.v
@@ -25,4 +25,4 @@ Next Obligation.
 Qed.
 
 Notation "×( C )" := (@InternalProductFunctor C _)
-  (at level 90, format "×( C )") : functor_scope.
+  (at level 0, format "×( C )") : functor_scope.
diff --git a/Functor/Structure/Monoidal/Pure.v b/Functor/Structure/Monoidal/Pure.v
index f1ba43f6..e09c443c 100644
--- a/Functor/Structure/Monoidal/Pure.v
+++ b/Functor/Structure/Monoidal/Pure.v
@@ -53,4 +53,4 @@ End Pure.
 Arguments pure {C _ F _ _ A}.
 
 Notation "pure[ F ]" := (@pure _ _ F _ _ _)
-  (at level 9, format "pure[ F ]") : morphism_scope.
+  (at level 0, format "pure[ F ]") : morphism_scope.
diff --git a/Instance/Coq/Applicative.v b/Instance/Coq/Applicative.v
index f8d0ddeb..4dbd297a 100644
--- a/Instance/Coq/Applicative.v
+++ b/Instance/Coq/Applicative.v
@@ -35,11 +35,11 @@ Arguments ap   {F _ _ _} _ x.
 
 Coercion Applicative_Functor `{@Applicative F} : Coq ⟶ Coq := F.
 
-Notation "pure[ F ]" := (@pure F _ _) (at level 19, F at next level).
-Notation "pure[ F G ]" := (@pure (fun x => F (G x)) _ _) (at level 9).
+Notation "pure[ F ]" := (@pure F _ _) (at level 0, F at next level).
+Notation "pure[ F G ]" := (@pure (fun x => F (G x)) _ _) (at level 0).
 
-Notation "ap[ F ]" := (@ap F _ _ _) (at level 9).
-Notation "ap[ F G ]" := (@ap (fun x => F (G x)) _ _ _) (at level 9).
+Notation "ap[ F ]" := (@ap F _ _ _) (at level 0).
+Notation "ap[ F G ]" := (@ap (fun x => F (G x)) _ _ _) (at level 0).
 
 Infix "<*>" := ap (at level 29, left associativity).
 Notation "x <**> F" := (ap F x) (at level 29, left associativity).
diff --git a/Theory/Coq/Applicative.v b/Theory/Coq/Applicative.v
index d23fcb3a..82d25c4e 100644
--- a/Theory/Coq/Applicative.v
+++ b/Theory/Coq/Applicative.v
@@ -28,16 +28,16 @@ Module ApplicativeNotations.
 Export FunctorNotations.
 
 Notation "pure[ M ]" := (@pure M _ _)
-  (at level 9, format "pure[ M ]").
+  (at level 0, format "pure[ M ]").
 Notation "pure[ M N ]" := (@pure (fun X => M (N X)) _ _)
-  (at level 9, format "pure[ M  N ]").
+  (at level 0, format "pure[ M  N ]").
 
 Notation "ap[ M ]" := (@ap M _ _ _)
-  (at level 9, format "ap[ M ]").
+  (at level 0, format "ap[ M ]").
 Notation "ap[ M N ]" := (@ap (fun X => M (N X)) _ _ _)
-  (at level 9, format "ap[ M  N ]").
+  (at level 0, format "ap[ M  N ]").
 Notation "ap[ M N O ]" := (@ap (fun X => M (N (O X))) _ _ _)
-  (at level 9, format "ap[ M  N  O ]").
+  (at level 0, format "ap[ M  N  O ]").
 
 Infix "<*>" := ap (at level 29, left associativity).
 Infix "<*[ M ]>" := (@ap M _ _ _)
diff --git a/Theory/Coq/Functor.v b/Theory/Coq/Functor.v
index c8bc2ee5..b046bfbc 100644
--- a/Theory/Coq/Functor.v
+++ b/Theory/Coq/Functor.v
@@ -32,22 +32,22 @@ Notation "x <&> f" := (fmap f x)
   (at level 29, left associativity, only parsing).
 
 Notation "fmap[ M ]" := (@fmap M _ _ _)
-  (at level 9, format "fmap[ M ]").
+  (at level 0, format "fmap[ M ]").
 Notation "fmap[ M N ]" := (@fmap (λ X, M (N X)) _ _ _)
-  (at level 9, format "fmap[ M  N ]").
+  (at level 0, format "fmap[ M  N ]").
 Notation "fmap[ M N O ]" := (@fmap (λ X, M (N (O X))) _ _ _)
-  (at level 9, format "fmap[ M  N  O ]").
+  (at level 0, format "fmap[ M  N  O ]").
 
 Infix ">$<" := contramap (at level 29, left associativity, only parsing).
 Notation "x >&< f" :=
   (contramap f x) (at level 29, left associativity, only parsing).
 
 Notation "contramap[ M ]" := (@contramap M _ _ _)
-  (at level 9, format "contramap[ M ]").
+  (at level 0, format "contramap[ M ]").
 Notation "contramap[ M N ]" := (@contramap (λ X, M (N X)) _ _ _)
-  (at level 9, format "contramap[ M  N ]").
+  (at level 0, format "contramap[ M  N ]").
 Notation "contramap[ M N O ]" := (@contramap (λ X, M (N (O X))) _ _ _)
-  (at level 9, format "contramap[ M  N  O ]").
+  (at level 0, format "contramap[ M  N  O ]").
 
 End FunctorNotations.
 
diff --git a/Theory/Functor.v b/Theory/Functor.v
index fa85500c..29f04219 100644
--- a/Theory/Functor.v
+++ b/Theory/Functor.v
@@ -57,9 +57,9 @@ Notation "x <&> f" := (fmap f x)
   (at level 29, left associativity, only parsing) : morphism_scope.
 
 Notation "fobj[ F ]" := (@fobj _ _ F%functor)
-  (at level 9, format "fobj[ F ]") : object_scope.
+  (at level 0, format "fobj[ F ]") : object_scope.
 Notation "fmap[ F ]" := (@fmap _ _ F%functor _ _)
-  (at level 9, format "fmap[ F ]") : morphism_scope.
+  (at level 0, format "fmap[ F ]") : morphism_scope.
 
 #[export] Hint Rewrite @fmap_id : categories.
 
@@ -168,7 +168,7 @@ Program Definition Id {C : Category} : C ⟶ C := {|
 
 Arguments Id {C} /.
 
-Notation "Id[ C ]" := (@Id C) (at level 9, format "Id[ C ]") : functor_scope.
+Notation "Id[ C ]" := (@Id C) (at level 0, format "Id[ C ]") : functor_scope.
 
 Program Definition Compose {C D E : Category}
         (F : D ⟶ E) (G : C ⟶ D) : C ⟶ E := {|

From 01f334cdf74439f8b998037d3af8d7c710b625a2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 29 Oct 2023 23:29:47 +0100
Subject: [PATCH 2/4] Extra parentheses needed in argument of a prefix notation
 at level 0.

---
 Instance/Cones/Limit.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Instance/Cones/Limit.v b/Instance/Cones/Limit.v
index 141a2c3e..6e5105c5 100644
--- a/Instance/Cones/Limit.v
+++ b/Instance/Cones/Limit.v
@@ -11,7 +11,7 @@ Program Definition Limit_Cones `(F : J ⟶ C) `{T : @Terminal (Cones F)} :
   Limit F := {|
   limit_cone := @terminal_obj _ T;
   ump_limits := fun N =>
-    {| unique_obj := `1 @one _ T N
-     ; unique_property := `2 @one _ T N
+    {| unique_obj := `1 (@one _ T N)
+     ; unique_property := `2 (@one _ T N)
      ; uniqueness       := fun v H => @one_unique _ T N (@one _ T N) (v; H) |}
 |}.

From e56751b0809433950ded08dd47577304da0d867f Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Sun, 5 Nov 2023 11:09:42 -0800
Subject: [PATCH 3/4] Define sites and sheaves

---
 Theory/Sheaf.v | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)

diff --git a/Theory/Sheaf.v b/Theory/Sheaf.v
index 721c213c..0de97ba8 100644
--- a/Theory/Sheaf.v
+++ b/Theory/Sheaf.v
@@ -3,6 +3,8 @@ Require Import Category.Theory.Category.
 Require Import Category.Theory.Functor.
 Require Import Category.Construction.Opposite.
 Require Import Category.Instance.Fun.
+Require Import Category.Instance.Sets.
+Require Import Coq.Vectors.Vector.
 
 Generalizable All Variables.
 
@@ -16,3 +18,69 @@ Definition Presheaves {U C : Category} := [U^op, C].
 Definition Copresheaf (U C : Category) := U ⟶ C.
 
 Definition Copresheaves {U C : Category} := [U, C].
+
+(* Custom data type to express Forall propositions on vectors over Type. *)
+Inductive ForallT {A : Type} (P : A → Type) :
+  ∀ {n : nat}, t A n → Type :=
+  | ForallT_nil : ForallT (nil A)
+  | ForallT_cons (n : nat) (x : A) (v : t A n) :
+    P x → ForallT v → ForallT (cons A x n v).
+
+(* A coverage on a category C consists of a function assigning to each object
+   U ∈ C a collection of families of morphisms { fᵢ : Uᵢ → U } (i∈I), called
+   covering families, such that
+
+   if { fᵢ : Uᵢ → U } (i∈I) is a covering family
+   and g : V → U is a morphism,
+   then there exists a covering family { hⱼ : Vⱼ → V }
+   such that each composite g ∘ hⱼ factors through some fᵢ. *)
+
+Class Site (C : Category) := {
+  covering_family (u : C) :=
+    ∃ I : nat, Vector.t (∃ v : C, v ~> u) I;
+
+  coverage (u : C) : covering_family u;
+
+  coverage_condition
+    (u  : C) (fs : covering_family u)
+    (v  : C) (g  : v ~> u) :
+    ∃ (hs : covering_family v),
+      ForallT
+        (λ h : { w : C & w ~> v },
+          ∃ (i : Fin.t (`1 fs)),
+            let f := Vector.nth (`2 fs) i in
+            ∃ (k : `1 h ~> `1 f),
+              `2 f ∘ k ≈ g ∘ `2 h)
+        (`2 hs)
+}.
+
+(* If { fᵢ : Uᵢ → U } (i∈I) is a family of morphisms with codomain U,
+   a presheaf X : Cᵒᵖ → Set is called a sheaf for this family if:
+
+   for any collection of elements xᵢ ∈ X(Uᵢ)
+   such that,
+     whenever g : V → Uᵢ and h : V → Uⱼ
+     are such that fᵢ ∘ g = fⱼ ∘ h,
+     we have X(g)(xᵢ) = X(h)(xⱼ),
+   then there exists a unique x ∈ X(U)
+   such that X(fᵢ)(x) = xᵢ for all i . *)
+
+Class Sheaf {C : Category} `{@Site C} (X : Presheaf C Sets) := {
+  restriction :
+    ∀ u : C,
+      let I := `1 (coverage u) in
+      let f := `2 (coverage u) in
+      ForallT
+        (λ fᵢ : { v : C & v ~> u },
+            ∀ (xᵢ : X (`1 fᵢ))
+              (P : ∀ (v : C)
+                     (g : v ~> `1 fᵢ)
+                     (j : Fin.t I),
+                  let fⱼ := Vector.nth f j in
+                  ∀ (h : v ~> `1 fⱼ),
+                    `2 fᵢ ∘ g ≈ `2 fⱼ ∘ h →
+                    ∀ xⱼ : X (`1 fⱼ),
+                      fmap[X] g xᵢ = fmap[X] h xⱼ),
+              ∃! x : X u, fmap[X] (`2 fᵢ) x = xᵢ)
+        f
+}.

From 856fdf621072f004f061428c5ad4c28ea3042d25 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Mon, 6 Nov 2023 08:33:29 -0800
Subject: [PATCH 4/4] Make the sheaf definition more succinct

---
 Theory/Sheaf.v | 51 +++++++++++++++++++++++++++-----------------------
 1 file changed, 28 insertions(+), 23 deletions(-)

diff --git a/Theory/Sheaf.v b/Theory/Sheaf.v
index 0de97ba8..2ae2bd16 100644
--- a/Theory/Sheaf.v
+++ b/Theory/Sheaf.v
@@ -26,6 +26,13 @@ Inductive ForallT {A : Type} (P : A → Type) :
   | ForallT_cons (n : nat) (x : A) (v : t A n) :
     P x → ForallT v → ForallT (cons A x n v).
 
+Inductive ExistsT {A : Type} (P : A → Type) :
+  ∀ {n : nat}, t A n → Type :=
+  | ExistsT_cons_hd (m : nat) (x : A) (v : t A m) :
+    P x → ExistsT (cons A x m v)
+  | ExistsT_cons_tl (m : nat) (x : A) (v : t A m) :
+    ExistsT v → ExistsT (cons A x m v).
+
 (* A coverage on a category C consists of a function assigning to each object
    U ∈ C a collection of families of morphisms { fᵢ : Uᵢ → U } (i∈I), called
    covering families, such that
@@ -36,21 +43,18 @@ Inductive ForallT {A : Type} (P : A → Type) :
    such that each composite g ∘ hⱼ factors through some fᵢ. *)
 
 Class Site (C : Category) := {
-  covering_family (u : C) :=
-    ∃ I : nat, Vector.t (∃ v : C, v ~> u) I;
+  covering_family (u : C) := sigT (Vector.t (∃ uᵢ, uᵢ ~> u));
 
   coverage (u : C) : covering_family u;
 
   coverage_condition
     (u  : C) (fs : covering_family u)
     (v  : C) (g  : v ~> u) :
-    ∃ (hs : covering_family v),
-      ForallT
-        (λ h : { w : C & w ~> v },
-          ∃ (i : Fin.t (`1 fs)),
-            let f := Vector.nth (`2 fs) i in
-            ∃ (k : `1 h ~> `1 f),
-              `2 f ∘ k ≈ g ∘ `2 h)
+    ∃ hs : covering_family v,
+      ForallT (A := ∃ vⱼ, vⱼ ~> v) (λ '(vⱼ; hⱼ),
+          ExistsT (A := ∃ uᵢ, uᵢ ~> u) (λ '(uᵢ; fᵢ),
+              ∃ k : vⱼ ~> uᵢ, fᵢ ∘ k ≈ g ∘ hⱼ)
+            (`2 fs))
         (`2 hs)
 }.
 
@@ -65,22 +69,23 @@ Class Site (C : Category) := {
    then there exists a unique x ∈ X(U)
    such that X(fᵢ)(x) = xᵢ for all i . *)
 
-Class Sheaf {C : Category} `{@Site C} (X : Presheaf C Sets) := {
+Class Sheaf `{@Site C} (X : Presheaf C Sets) := {
   restriction :
     ∀ u : C,
-      let I := `1 (coverage u) in
-      let f := `2 (coverage u) in
+      let '(i; f) := coverage u in
       ForallT
-        (λ fᵢ : { v : C & v ~> u },
-            ∀ (xᵢ : X (`1 fᵢ))
-              (P : ∀ (v : C)
-                     (g : v ~> `1 fᵢ)
-                     (j : Fin.t I),
-                  let fⱼ := Vector.nth f j in
-                  ∀ (h : v ~> `1 fⱼ),
-                    `2 fᵢ ∘ g ≈ `2 fⱼ ∘ h →
-                    ∀ xⱼ : X (`1 fⱼ),
-                      fmap[X] g xᵢ = fmap[X] h xⱼ),
-              ∃! x : X u, fmap[X] (`2 fᵢ) x = xᵢ)
+        (A := ∃ uᵢ, uᵢ ~> u)
+        (λ '(uᵢ; fᵢ),
+            ∀ xᵢ : X uᵢ,
+              (∀ (v : C) (g : v ~> uᵢ),
+                  ForallT
+                    (A := ∃ uⱼ, uⱼ ~> u)
+                    (λ '(uⱼ; fⱼ),
+                      ∀ h : v ~> uⱼ,
+                        fᵢ ∘ g ≈ fⱼ ∘ h →
+                        ∀ xⱼ : X uⱼ,
+                          fmap[X] g xᵢ = fmap[X] h xⱼ)
+                    f) →
+              ∃! x : X u, fmap[X] fᵢ x = xᵢ)
         f
 }.