From bd6f5dee80aec04c72452c99a3a0a39c94cf4b73 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 21 Nov 2023 10:19:34 +0100
Subject: [PATCH] Sites, sheaves and sheafification as a QIT (#1031)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
* stubs for Coverage, Cover, Sieve
* covers as families, sieves
* pulledBackSieve
* finish Coverage
* slightly simplify generatedSieve
* universal property of generatedSieve
* make C implicit in sieve operations
* make C implicit in patchArr and patchObj
* definition of sheaves on a site
* tiny improvement (qualified import)
* remove unnecessary parenthesis
* indentation in equational reasoning
* sheafification QIT
* correct silly mistake
* rename CompatibleFamilies -> CompatibleFamily
* sheafification is a sheaf
* rename
* stub of the universal property
* small renaming
* (wip)
* (wip) (termination checker problems)
* (wip) solved termination issue
thanks to Ingo Blechschmidt!
* finish inducedMap of sheafification
* comment with reference
* rename i -> patch
* diagram comment and a bit of preparation
* elimProp with restrictPreservesB
* introduce isSeparated
* uniqueness part of universal property
* package up as universal element
* name constructor arguments
* elimProp without restrictPreservesB assumption
* prepare for merging module
* merge module
* properly name elimProp assumptions
* fix misnomer (now we have (η ⟦ _ ⟧) x = η⟦⟧ x)
* structure elimPropInduction more nicely
* fix indentation
* use improved elimProp in uniqueness
* split sheafification in several files
* clean up imports
* eliminate Families by inlining
* comments in ElimProp
* references for coverage
* make two arguments implicit
* a few more comments
* fix unresolved meta (with Agda 2.6.3)
* make helpers private
* let isSheaf be an hProp
* fix naming typo
* un-bundle `hProp`s in `Sheaf.agda`
* un-bundle `hProp`s in `Sieve.agda`
* rename `F` -> `sheafification`
* also rename the HIT `⟨F⟅_⟆⟩` and the local `F`
* elaborate universe level comment
---
Cubical/Categories/Site/Cover.agda | 44 ++++
Cubical/Categories/Site/Coverage.agda | 43 ++++
Cubical/Categories/Site/Sheaf.agda | 138 ++++++++++++
Cubical/Categories/Site/Sheafification.agda | 6 +
.../Categories/Site/Sheafification/Base.agda | 126 +++++++++++
.../Site/Sheafification/ElimProp.agda | 208 ++++++++++++++++++
.../Sheafification/UniversalProperty.agda | 188 ++++++++++++++++
Cubical/Categories/Site/Sieve.agda | 124 +++++++++++
8 files changed, 877 insertions(+)
create mode 100644 Cubical/Categories/Site/Cover.agda
create mode 100644 Cubical/Categories/Site/Coverage.agda
create mode 100644 Cubical/Categories/Site/Sheaf.agda
create mode 100644 Cubical/Categories/Site/Sheafification.agda
create mode 100644 Cubical/Categories/Site/Sheafification/Base.agda
create mode 100644 Cubical/Categories/Site/Sheafification/ElimProp.agda
create mode 100644 Cubical/Categories/Site/Sheafification/UniversalProperty.agda
create mode 100644 Cubical/Categories/Site/Sieve.agda
diff --git a/Cubical/Categories/Site/Cover.agda b/Cubical/Categories/Site/Cover.agda
new file mode 100644
index 0000000000..ae6c7ea719
--- /dev/null
+++ b/Cubical/Categories/Site/Cover.agda
@@ -0,0 +1,44 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Cover where
+
+-- A cover of an object is just a family of arrows into that object.
+-- This notion is used in the definition of a coverage.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Constructions.Slice
+
+
+module _
+ {ℓ ℓ' : Level}
+ (C : Category ℓ ℓ')
+ where
+
+ open Category
+
+ Cover : (ℓpat : Level) → ob C → Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓpat))
+ Cover ℓpat c = TypeWithStr ℓpat λ patches → patches → ob (SliceCat C c)
+
+module _
+ {ℓ ℓ' : Level}
+ {C : Category ℓ ℓ'}
+ where
+
+ open Category
+
+ -- Extracting the members (patches) from a cover.
+ module _
+ {ℓpat : Level}
+ {c : ob C}
+ (cov : Cover C ℓpat c)
+ (patch : ⟨ cov ⟩)
+ where
+
+ patchObj : ob C
+ patchObj = S-ob (str cov patch)
+
+ patchArr : C [ patchObj , c ]
+ patchArr = S-arr (str cov patch)
diff --git a/Cubical/Categories/Site/Coverage.agda b/Cubical/Categories/Site/Coverage.agda
new file mode 100644
index 0000000000..5e581ef2bf
--- /dev/null
+++ b/Cubical/Categories/Site/Coverage.agda
@@ -0,0 +1,43 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Coverage where
+
+-- Definition of a coverage on a category, also called a Grothendieck topology.
+-- A coverage on a category turns it into a site
+-- and enables us to formulate a sheaf condition.
+
+-- We stay close to the definitions given in the nLab and the Elephant:
+-- * https://ncatlab.org/nlab/show/coverage
+-- * Peter Johnstone, "Sketches of an Elephant" (Definition C2.1.1)
+
+-- While the covers are just families of arrows,
+-- we use the notion of sieves to express the "pullback stability" property of the coverage.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Sieve
+
+module _
+ {ℓ ℓ' : Level}
+ (C : Category ℓ ℓ')
+ where
+
+ open Category C
+
+ record Coverage (ℓcov ℓpat : Level) : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-suc (ℓ-max ℓcov ℓpat)))) where
+ no-eta-equality
+ field
+ covers : (c : ob) → TypeWithStr ℓcov λ Cov → Cov → (Cover C ℓpat c)
+ pullbackStability :
+ {c : ob} →
+ (cov : ⟨ covers c ⟩) →
+ {d : ob} →
+ (f : Hom[ d , c ]) →
+ ∃[ cov' ∈ ⟨ covers d ⟩ ]
+ coverRefinesSieve
+ (str (covers d) cov')
+ (pulledBackSieve f (generatedSieve (str (covers c) cov)))
diff --git a/Cubical/Categories/Site/Sheaf.agda b/Cubical/Categories/Site/Sheaf.agda
new file mode 100644
index 0000000000..c1fa5b53ac
--- /dev/null
+++ b/Cubical/Categories/Site/Sheaf.agda
@@ -0,0 +1,138 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheaf where
+
+-- Definition of sheaves on a site.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function using (_∘_)
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Functions.Embedding
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Sieve
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.FullSubcategory
+
+module _
+ {ℓ ℓ' : Level}
+ {C : Category ℓ ℓ'}
+ {ℓP : Level}
+ (P : Presheaf C ℓP)
+ where
+
+ open Category C hiding (_∘_)
+
+ module _
+ {c : ob}
+ {ℓ'' : Level}
+ (cov : Cover C ℓ'' c)
+ where
+
+ FamilyOnCover : Type (ℓ-max ℓP ℓ'')
+ FamilyOnCover = (i : ⟨ cov ⟩) → ⟨ P ⟅ patchObj cov i ⟆ ⟩
+
+ isCompatibleFamily : FamilyOnCover → Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓP) ℓ'')
+ isCompatibleFamily fam =
+ (i : ⟨ cov ⟩) →
+ (j : ⟨ cov ⟩) →
+ (d : ob) →
+ (f : Hom[ d , patchObj cov i ]) →
+ (g : Hom[ d , patchObj cov j ]) →
+ f ⋆ patchArr cov i ≡ g ⋆ patchArr cov j →
+ (P ⟪ f ⟫) (fam i) ≡ (P ⟪ g ⟫) (fam j)
+
+ isPropIsCompatibleFamily : (fam : FamilyOnCover) → isProp (isCompatibleFamily fam)
+ isPropIsCompatibleFamily fam =
+ isPropΠ6 λ _ _ d _ _ _ → str (P ⟅ d ⟆) _ _
+
+ CompatibleFamily : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓP) ℓ'')
+ CompatibleFamily = Σ FamilyOnCover isCompatibleFamily
+
+ isSetCompatibleFamily : isSet CompatibleFamily
+ isSetCompatibleFamily =
+ isSetΣSndProp
+ (isSetΠ (λ i → str (P ⟅ patchObj cov i ⟆)))
+ isPropIsCompatibleFamily
+
+ elementToCompatibleFamily : ⟨ P ⟅ c ⟆ ⟩ → CompatibleFamily
+ elementToCompatibleFamily x =
+ (λ i → (P ⟪ patchArr cov i ⟫) x) ,
+ λ i j d f g eq → cong (λ f → f x) (
+ P ⟪ f ⟫ ∘ P ⟪ patchArr cov i ⟫ ≡⟨ sym (F-seq (patchArr cov i) f ) ⟩
+ P ⟪ f ⋆ patchArr cov i ⟫ ≡⟨ cong (P ⟪_⟫) eq ⟩
+ P ⟪ g ⋆ patchArr cov j ⟫ ≡⟨ F-seq (patchArr cov j) g ⟩
+ P ⟪ g ⟫ ∘ P ⟪ patchArr cov j ⟫ ∎ )
+ where
+ open Functor P
+
+ hasAmalgamationPropertyForCover : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓP) ℓ'')
+ hasAmalgamationPropertyForCover =
+ isEquiv elementToCompatibleFamily
+
+ isPropHasAmalgamationPropertyForCover : isProp hasAmalgamationPropertyForCover
+ isPropHasAmalgamationPropertyForCover =
+ isPropIsEquiv _
+
+module _
+ {ℓ ℓ' ℓcov ℓpat : Level}
+ {C : Category ℓ ℓ'}
+ (J : Coverage C ℓcov ℓpat)
+ {ℓP : Level}
+ (P : Presheaf C ℓP)
+ where
+
+ open Coverage J
+
+ isSeparated : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓcov) ℓpat) ℓP)
+ isSeparated =
+ (c : _) →
+ (cov : ⟨ covers c ⟩) →
+ (x : ⟨ P ⟅ c ⟆ ⟩) →
+ (y : ⟨ P ⟅ c ⟆ ⟩) →
+ ( (patch : _) →
+ let f = patchArr (str (covers c) cov) patch
+ in (P ⟪ f ⟫) x ≡ (P ⟪ f ⟫) y ) →
+ x ≡ y
+
+ isPropIsSeparated : isProp isSeparated
+ isPropIsSeparated = isPropΠ5 (λ c _ _ _ _ → str (P ⟅ c ⟆) _ _)
+
+ isSheaf : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP)
+ isSheaf =
+ (c : _) →
+ (cov : ⟨ covers c ⟩) →
+ hasAmalgamationPropertyForCover P (str (covers c) cov)
+
+ isPropIsSheaf : isProp isSheaf
+ isPropIsSheaf = isPropΠ2 λ c cov → isPropHasAmalgamationPropertyForCover P (str (covers c) cov)
+
+ isSheaf→isSeparated : isSheaf → isSeparated
+ isSheaf→isSeparated isSheafP c cov x y locallyEqual =
+ isEmbedding→Inj (isEquiv→isEmbedding (isSheafP c cov)) x y
+ (Σ≡Prop
+ (isPropIsCompatibleFamily {C = C} P _)
+ (funExt locallyEqual))
+
+module _
+ {ℓ ℓ' ℓcov ℓpat : Level}
+ {C : Category ℓ ℓ'}
+ (J : Coverage C ℓcov ℓpat)
+ (ℓF : Level)
+ where
+
+ Sheaf : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) (ℓ-suc ℓF))
+ Sheaf = Σ[ P ∈ Presheaf C ℓF ] isSheaf J P
+
+ SheafCategory :
+ Category
+ (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) (ℓ-suc ℓF))
+ (ℓ-max (ℓ-max ℓ ℓ') ℓF)
+ SheafCategory = FullSubcategory (PresheafCategory C ℓF) (isSheaf J)
diff --git a/Cubical/Categories/Site/Sheafification.agda b/Cubical/Categories/Site/Sheafification.agda
new file mode 100644
index 0000000000..43862edcad
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification where
+
+open import Cubical.Categories.Site.Sheafification.Base public
+open import Cubical.Categories.Site.Sheafification.ElimProp public
+open import Cubical.Categories.Site.Sheafification.UniversalProperty public
diff --git a/Cubical/Categories/Site/Sheafification/Base.agda b/Cubical/Categories/Site/Sheafification/Base.agda
new file mode 100644
index 0000000000..1f78c48c07
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification/Base.agda
@@ -0,0 +1,126 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification.Base where
+
+-- Construction of the sheafification of a presheaf on a site
+-- using a quotient inductive type (QIT).
+
+-- This is inspired by the construction of the sheafification (for finite coverings) in:
+-- * E. Palmgren, S.J. Vickers, "Partial Horn logic and cartesian categories"
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function using (_∘_)
+
+open import Cubical.HITs.PropositionalTruncation using (∣_∣₁)
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Functions.Surjection
+open import Cubical.Functions.Embedding
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Site.Sheaf
+
+
+module Sheafification
+ {ℓ ℓ' ℓcov ℓpat : Level}
+ {C : Category ℓ ℓ'}
+ (J : Coverage C ℓcov ℓpat)
+ {ℓP : Level}
+ (P : Presheaf C ℓP)
+ where
+
+ open Category C hiding (_∘_)
+ open Coverage J
+
+ data ⟨sheafification⟅_⟆⟩ : ob → Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓcov (ℓ-max ℓpat ℓP)))) where
+
+ trunc : {c : ob} → isSet ⟨sheafification⟅ c ⟆⟩
+
+ restrict : {c d : ob} → (f : Hom[ d , c ]) → ⟨sheafification⟅ c ⟆⟩ → ⟨sheafification⟅ d ⟆⟩
+
+ restrictId :
+ {c : ob} →
+ (x : ⟨sheafification⟅ c ⟆⟩) →
+ restrict id x ≡ x
+ restrictRestrict :
+ {c d e : ob} →
+ (f : Hom[ d , c ]) →
+ (g : Hom[ e , d ]) →
+ (x : ⟨sheafification⟅ c ⟆⟩) →
+ restrict (g ⋆ f) x ≡ restrict g (restrict f x)
+
+ η⟦⟧ : {c : ob} → (x : ⟨ P ⟅ c ⟆ ⟩) → ⟨sheafification⟅ c ⟆⟩
+
+ ηNatural :
+ {c d : ob} →
+ (f : Hom[ d , c ]) →
+ (x : ⟨ P ⟅ c ⟆ ⟩) →
+ η⟦⟧ ((P ⟪ f ⟫) x) ≡ restrict f (η⟦⟧ x)
+
+ sep :
+ {c : ob} →
+ (cover : ⟨ covers c ⟩) →
+ let cov = str (covers c) cover in
+ (x y : ⟨sheafification⟅ c ⟆⟩) →
+ (x~y :
+ (patch : ⟨ cov ⟩) →
+ restrict (patchArr cov patch) x ≡ restrict (patchArr cov patch) y) →
+ x ≡ y
+
+ amalgamate :
+ let
+ -- Is there any way to make this definition now and reuse it later?
+ sheafification : Presheaf C _
+ sheafification = record
+ { F-ob = λ c → ⟨sheafification⟅ c ⟆⟩ , trunc
+ ; F-hom = restrict
+ ; F-id = funExt restrictId
+ ; F-seq = λ f g → funExt (restrictRestrict f g)
+ }
+ in
+ {c : ob} →
+ (cover : ⟨ covers c ⟩) →
+ let cov = str (covers c) cover in
+ (fam : CompatibleFamily sheafification cov) →
+ ⟨sheafification⟅ c ⟆⟩
+ restrictAmalgamate :
+ let
+ sheafification : Presheaf C _
+ sheafification = record
+ { F-ob = λ c → ⟨sheafification⟅ c ⟆⟩ , trunc
+ ; F-hom = restrict
+ ; F-id = funExt restrictId
+ ; F-seq = λ f g → funExt (restrictRestrict f g)
+ }
+ in
+ {c : ob} →
+ (cover : ⟨ covers c ⟩) →
+ let cov = str (covers c) cover in
+ (fam : CompatibleFamily sheafification cov) →
+ (patch : ⟨ cov ⟩) →
+ restrict (patchArr cov patch) (amalgamate cover fam) ≡ fst fam patch
+
+ sheafification : Presheaf C (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP)
+ Functor.F-ob sheafification c = ⟨sheafification⟅ c ⟆⟩ , trunc
+ Functor.F-hom sheafification = restrict
+ Functor.F-id sheafification = funExt restrictId
+ Functor.F-seq sheafification f g = funExt (restrictRestrict f g)
+
+ isSheafSheafification : isSheaf J sheafification
+ isSheafSheafification c cover = isEmbedding×isSurjection→isEquiv
+ ( injEmbedding
+ (isSetCompatibleFamily sheafification cov)
+ (λ {x} {y} x~y → sep cover x y (funExt⁻ (cong fst x~y)))
+ , λ fam →
+ ∣ amalgamate cover fam
+ , Σ≡Prop
+ (isPropIsCompatibleFamily sheafification cov)
+ (funExt (restrictAmalgamate cover fam)) ∣₁ )
+ where
+ cov = str (covers c) cover
diff --git a/Cubical/Categories/Site/Sheafification/ElimProp.agda b/Cubical/Categories/Site/Sheafification/ElimProp.agda
new file mode 100644
index 0000000000..0e5dd855ac
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification/ElimProp.agda
@@ -0,0 +1,208 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification.ElimProp where
+
+-- An elimination operator from the QIT definition of sheafification
+-- into a dependent proposition.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+
+import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Site.Sheaf
+
+open import Cubical.Categories.Site.Sheafification.Base
+
+
+module _
+ {ℓ ℓ' ℓcov ℓpat : Level}
+ {C : Category ℓ ℓ'}
+ (J : Coverage C ℓcov ℓpat)
+ {ℓP : Level}
+ (P : Presheaf C ℓP)
+ where
+
+ open Category C
+ open Coverage J
+ open Sheafification J P
+
+ -- We name the (potential) assumptions on 'B' here to avoid repetition.
+ module ElimPropAssumptions
+ {ℓB : Level}
+ (B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB)
+ where
+
+ isPropValued =
+ {c : ob} →
+ {x : ⟨ sheafification ⟅ c ⟆ ⟩} →
+ isProp (B x)
+
+ Onη =
+ {c : ob} →
+ (x : ⟨ P ⟅ c ⟆ ⟩) →
+ B (η⟦⟧ x)
+
+ -- This way to say that 'B' respects the 'amalgamate' point constructor
+ -- should usually be more convenient to prove.
+ isLocal =
+ {c : ob} →
+ (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
+ (cover : ⟨ covers c ⟩) →
+ let cov = str (covers c) cover in
+ ((patch : ⟨ cov ⟩) → B (restrict (patchArr cov patch) x)) →
+ B x
+
+ -- This assumption will turn out to be unnecessary.
+ isMonotonous =
+ {c d : ob} →
+ (f : Hom[ d , c ]) →
+ (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
+ B x → B (restrict f x)
+
+ open ElimPropAssumptions
+
+ -- A fist version of elimProp that uses the isMonotonous assumption.
+ module ElimPropWithMonotonous
+ {ℓB : Level}
+ {B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB}
+ (isPropValuedB : isPropValued B)
+ (onηB : Onη B)
+ (isLocalB : isLocal B)
+ (isMonotonousB : isMonotonous B)
+ where
+
+ -- We have to transform the 'isLocal' assumption into the actual statement
+ -- that 'B' respects 'amalgamate'.
+ amalgamatePreservesB :
+ {c : ob} →
+ (cover : ⟨ covers c ⟩) →
+ let cov = str (covers c) cover in
+ (fam : CompatibleFamily sheafification cov) →
+ ((patch : ⟨ cov ⟩) → B (fst fam patch)) →
+ B (amalgamate cover fam)
+ amalgamatePreservesB cover fam famB =
+ isLocalB
+ (amalgamate cover fam)
+ cover
+ λ patch → subst B (sym (restrictAmalgamate cover fam patch)) (famB patch)
+
+ -- A helper to deal with the path constructor cases.
+ mkPathP :
+ {c : ob} →
+ {x0 x1 : ⟨ sheafification ⟅ c ⟆ ⟩} →
+ (p : x0 ≡ x1) →
+ (b0 : B (x0)) →
+ (b1 : B (x1)) →
+ PathP (λ i → B (p i)) b0 b1
+ mkPathP p = isProp→PathP (λ i → isPropValuedB)
+
+ elimProp : {c : ob} → (x : ⟨ sheafification ⟅ c ⟆ ⟩) → B x
+ elimProp (trunc x y p q i j) =
+ isOfHLevel→isOfHLevelDep 2 (λ _ → isProp→isSet isPropValuedB)
+ (elimProp x)
+ (elimProp y)
+ (cong elimProp p)
+ (cong elimProp q)
+ (trunc x y p q)
+ i
+ j
+ elimProp (restrict f x) =
+ isMonotonousB f x (elimProp x)
+ elimProp (restrictId x i) =
+ mkPathP
+ (restrictId x)
+ (isMonotonousB id x (elimProp x))
+ (elimProp x)
+ i
+ elimProp (restrictRestrict f g x i) =
+ mkPathP (restrictRestrict f g x)
+ (isMonotonousB (g ⋆ f) x (elimProp x))
+ (isMonotonousB g (restrict f x) (isMonotonousB f x (elimProp x)))
+ i
+ elimProp (η⟦⟧ x) =
+ onηB x
+ elimProp (ηNatural f x i) =
+ mkPathP (ηNatural f x)
+ (onηB ((P ⟪ f ⟫) x))
+ (isMonotonousB f (η⟦⟧ x) (onηB x))
+ i
+ elimProp (sep cover x y x~y i) =
+ mkPathP (sep cover x y x~y)
+ (elimProp x)
+ (elimProp y)
+ i
+ elimProp (amalgamate cover fam) =
+ amalgamatePreservesB cover fam λ patch → elimProp (fst fam patch)
+ elimProp (restrictAmalgamate cover fam patch i) =
+ let cov = str (covers _) cover in
+ mkPathP (restrictAmalgamate cover fam patch)
+ (isMonotonousB (patchArr cov patch) (amalgamate cover fam)
+ (amalgamatePreservesB cover fam (λ patch' → elimProp (fst fam patch'))))
+ (elimProp (fst fam patch))
+ i
+
+ -- Now we drop the 'isMonotonous' assumption and prove the stronger version of 'elimProp'.
+ module _
+ {ℓB : Level}
+ {B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB}
+ (isPropValuedB : isPropValued B)
+ (onηB : Onη B)
+ (isLocalB : isLocal B)
+ where
+
+ -- Idea: strengthen the inductive hypothesis to "every restriction of x satisfies 'B'"
+ private
+ B' : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type (ℓ-max (ℓ-max ℓ ℓ') ℓB)
+ B' x = {d : ob} → (f : Hom[ d , _ ]) → B (restrict f x)
+
+ isPropValuedB' : isPropValued B'
+ isPropValuedB' = isPropImplicitΠ λ _ → isPropΠ λ _ → isPropValuedB
+
+ onηB' : Onη B'
+ onηB' x f = subst B (ηNatural f x) (onηB ((P ⟪ f ⟫) x))
+
+ isLocalB' : isLocal B'
+ isLocalB' x cover B'fam f =
+ PT.rec
+ isPropValuedB
+ (λ (cover' , refines) →
+ isLocalB (restrict f x) cover' λ patch' →
+ PT.rec
+ isPropValuedB
+ (λ (patch , g , p'⋆f≡g⋆p) →
+ let
+ p = patchArr (str (covers _) cover) patch
+ p' = patchArr (str (covers _) cover') patch'
+ in
+ subst B
+ ( restrict g (restrict p x) ≡⟨ sym (restrictRestrict _ _ _) ⟩
+ restrict (g ⋆ p) x ≡⟨ cong (λ f → restrict f x) (sym p'⋆f≡g⋆p) ⟩
+ restrict (p' ⋆ f) x ≡⟨ restrictRestrict _ _ _ ⟩
+ restrict p' (restrict f x) ∎ )
+ (B'fam patch g))
+ (refines patch'))
+ (pullbackStability cover f)
+
+ isMonotonousB' : isMonotonous B'
+ isMonotonousB' f x B'x g = subst B (restrictRestrict _ _ _) (B'x (g ⋆ f))
+
+ elimPropInduction :
+ {c : ob} →
+ (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
+ B' x
+ elimPropInduction =
+ ElimPropWithMonotonous.elimProp {B = B'}
+ isPropValuedB'
+ onηB'
+ isLocalB'
+ isMonotonousB'
+
+ elimProp : {c : ob} → (x : ⟨ sheafification ⟅ c ⟆ ⟩) → B x
+ elimProp x = subst B (restrictId _) (elimPropInduction x id)
diff --git a/Cubical/Categories/Site/Sheafification/UniversalProperty.agda b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
new file mode 100644
index 0000000000..8fd6714028
--- /dev/null
+++ b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
@@ -0,0 +1,188 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sheafification.UniversalProperty where
+
+-- We prove the universal property of the sheafification,
+-- exhibiting it as a left adjoint to the forgetful functor.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function using (_$_; _∘_)
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Constructions.FullSubcategory
+
+open import Cubical.Categories.Site.Cover
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Site.Sheaf
+
+open import Cubical.Categories.Site.Sheafification.Base
+open import Cubical.Categories.Site.Sheafification.ElimProp
+
+
+module UniversalProperty
+ {ℓ ℓ' ℓcov ℓpat : Level}
+ {C : Category ℓ ℓ'}
+ (J : Coverage C ℓcov ℓpat)
+ where
+
+ -- We assume 'P' to have the following universe level in order to ensure that
+ -- the sheafification does not raise the universe level.
+ -- This is unfortunately necessary as long as we want to use the general
+ -- definition of natural transformations for the maps between presheaves.
+ -- (Other than that, the sheafification construction should enjoy the expected
+ -- universal property also for 'P' of arbitrary universe level.)
+ ℓP = ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓcov ℓpat))
+
+ module _
+ (P : Presheaf C ℓP)
+ where
+
+ open Category C hiding (_∘_)
+
+ private
+ C^ = PresheafCategory C ℓP
+ module C^ = Category C^
+
+ open Coverage J
+ open Sheafification J P
+ open NatTrans
+ open Functor
+
+ η : P ⇒ sheafification
+ N-ob η c = η⟦⟧
+ N-hom η f = funExt (ηNatural f)
+
+ module InducedMap
+ (G : Presheaf C ℓP)
+ (isSheafG : isSheaf J G)
+ (α : P ⇒ G)
+ where
+
+{-
+ η
+ P --> sheafification
+ \ .
+ \ . inducedMap
+ α \ .
+ ∨ ∨
+ G
+-}
+
+ private
+
+ ν : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → ⟨ G ⟅ c ⟆ ⟩
+
+ ν (trunc x y p q i j) = str (G ⟅ _ ⟆) _ _ (cong ν p) (cong ν q) i j
+ ν (restrict f x) = (G ⟪ f ⟫) (ν x)
+ ν (restrictId x i) = funExt⁻ (F-id G) (ν x) i
+ ν (restrictRestrict {c} {d} {e} f g x i) = funExt⁻ (F-seq G f g) (ν x) i
+ ν (η⟦⟧ x) = (α ⟦ _ ⟧) x
+ ν (ηNatural f x i) = funExt⁻ (N-hom α f) x i
+
+ ν (sep cover x y x~y i) =
+ isSheaf→isSeparated J G isSheafG _ cover
+ (ν x)
+ (ν y)
+ (λ patch → cong ν (x~y patch))
+ i
+ where
+ cov = str (covers _) cover
+
+ ν (amalgamate cover (fam , compat)) =
+ fst (fst (equiv-proof (isSheafG _ cover) fam'))
+ where
+ cov = str (covers _) cover
+ -- We have to push forward 'fam' along the natural transformation 'ν' that we are just defining.
+ fam' : CompatibleFamily G cov
+ fam' =
+ (λ i → ν (fam i)) ,
+ λ i j d f g diamond → cong ν (compat i j d f g diamond)
+
+ ν (restrictAmalgamate cover (fam , compat) patch i) =
+ fst (snd (fst (equiv-proof (isSheafG _ cover) fam')) i) patch
+ where
+ cov = str (covers _) cover
+ fam' : CompatibleFamily G cov
+ fam' =
+ (λ i → ν (fam i)) ,
+ λ i j d f g diamond → cong ν (compat i j d f g diamond)
+
+ inducedMap : sheafification ⇒ G
+ N-ob inducedMap c = ν
+ N-hom inducedMap f = refl
+
+ inducedMapFits : η C^.⋆ inducedMap ≡ α
+ inducedMapFits = makeNatTransPath refl
+
+ module _
+ (β : sheafification ⇒ G)
+ (βFits : η C^.⋆ β ≡ α)
+ where
+
+ open ElimPropAssumptions J P
+
+ private
+ B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type _
+ B x = (β ⟦ _ ⟧) x ≡ ν x
+
+ isPropValuedB : isPropValued B
+ isPropValuedB = str (G ⟅ _ ⟆) _ _
+
+ onηB : Onη B
+ onηB = funExt⁻ (funExt⁻ (cong N-ob βFits) _)
+
+ isLocalB : isLocal B
+ isLocalB x cover locallyAgree =
+ isSheaf→isSeparated J G isSheafG _ cover
+ ((β ⟦ _ ⟧) x)
+ (ν x)
+ λ patch →
+ let f = patchArr (str (covers _) cover) patch in
+ (G ⟪ f ⟫) ((β ⟦ _ ⟧) x) ≡⟨ sym (cong (_$ x) (N-hom β f)) ⟩
+ ((β ⟦ _ ⟧) ((sheafification ⟪ f ⟫) x)) ≡⟨ locallyAgree patch ⟩
+ (G ⟪ f ⟫) (ν x) ∎
+
+ uniqueness : β ≡ inducedMap
+ uniqueness = makeNatTransPath (funExt λ _ → funExt (
+ elimProp J P {B = B} isPropValuedB onηB isLocalB))
+
+ -- This alternative proof does not use the 'pullbackStability' of the coverage.
+ module _ where private
+
+ isMonotonousB : isMonotonous B
+ isMonotonousB f x βx≡νx =
+ (β ⟦ _ ⟧) (restrict f x) ≡⟨ cong (_$ x) (N-hom β f) ⟩
+ (G ⟪ f ⟫) ((β ⟦ _ ⟧) x) ≡⟨ cong (G ⟪ f ⟫) βx≡νx ⟩
+ (G ⟪ f ⟫) (ν x) ∎
+
+ uniqueness' : β ≡ inducedMap
+ uniqueness' = makeNatTransPath (funExt λ _ → funExt (
+ ElimPropWithMonotonous.elimProp J P
+ {B = B}
+ isPropValuedB
+ onηB
+ isLocalB
+ isMonotonousB))
+
+ sheafificationIsUniversal :
+ isUniversal
+ (SheafCategory J ℓP ^op)
+ ((C^ [ P ,-]) ∘F FullInclusion C^ (isSheaf J))
+ (sheafification , isSheafSheafification)
+ η
+ sheafificationIsUniversal (G , isSheafG) = record
+ { equiv-proof = λ α →
+ let open InducedMap G isSheafG α in
+ (inducedMap , inducedMapFits)
+ , λ (β , βFits) →
+ Σ≡Prop
+ (λ _ → C^.isSetHom _ _)
+ (sym (uniqueness β βFits))
+ }
diff --git a/Cubical/Categories/Site/Sieve.agda b/Cubical/Categories/Site/Sieve.agda
new file mode 100644
index 0000000000..183b6240f4
--- /dev/null
+++ b/Cubical/Categories/Site/Sieve.agda
@@ -0,0 +1,124 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Site.Sieve where
+
+-- Definition of sieves on an object
+-- and the sieve generated by a cover.
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Site.Cover
+
+module _
+ {ℓ ℓ' : Level}
+ (C : Category ℓ ℓ')
+ where
+
+ open Category C
+
+ record Sieve (ℓsie : Level) (c : ob) : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-suc ℓsie))) where
+ no-eta-equality
+ field
+ passes : {d : ob} → Hom[ d , c ] → Type ℓsie
+ isPropPasses : {d : ob} → (f : Hom[ d , c ]) → isProp (passes f)
+ closedUnderPrecomposition :
+ {d' d : ob} (p : Hom[ d' , d ]) (f : Hom[ d , c ]) →
+ passes f → passes (p ⋆ f)
+
+
+module _
+ {ℓ ℓ' : Level}
+ {C : Category ℓ ℓ'}
+ where
+
+ open Category C hiding (_∘_)
+ open Sieve
+
+ sieveRefinesSieve :
+ {ℓS' ℓS : Level} →
+ {c : ob} →
+ Sieve C ℓS' c →
+ Sieve C ℓS c →
+ Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓS') ℓS)
+ sieveRefinesSieve S' S =
+ (d : ob) →
+ (f : Hom[ d , _ ]) →
+ passes S' f → passes S f
+
+ isPropSieveRefinesSieve :
+ {ℓS' ℓS : Level} →
+ {c : ob} →
+ (S : Sieve C ℓS' c) →
+ (S' : Sieve C ℓS c) →
+ isProp (sieveRefinesSieve S S')
+ isPropSieveRefinesSieve S S' =
+ isPropΠ3 (λ d f _ → isPropPasses S' f)
+
+ generatedSieve : {ℓ : Level} {c : ob} → Cover C ℓ c → Sieve C (ℓ-max ℓ' ℓ) c
+ passes (generatedSieve cov) f =
+ ∃[ i ∈ ⟨ cov ⟩ ] Σ[ h ∈ Hom[ _ , _ ] ] f ≡ h ⋆ patchArr cov i
+ isPropPasses (generatedSieve cov) f = isPropPropTrunc
+ closedUnderPrecomposition (generatedSieve cov) p f =
+ PT.rec isPropPropTrunc λ (i , h , f≡hi) →
+ ∣ i
+ , (p ⋆ h)
+ , ( (p ⋆ f) ≡⟨ cong (p ⋆_) f≡hi ⟩
+ (p ⋆ (h ⋆ patchArr cov i)) ≡⟨ sym (⋆Assoc p h (patchArr cov i)) ⟩
+ ((p ⋆ h) ⋆ patchArr cov i) ∎ )
+ ∣₁
+
+ coverRefinesSieve :
+ {ℓcov ℓsie : Level}
+ {c : ob} →
+ Cover C ℓcov c →
+ Sieve C ℓsie c →
+ Type (ℓ-max ℓcov ℓsie)
+ coverRefinesSieve cov S =
+ (i : _) → passes S (patchArr cov i)
+
+ isPropCoverRefinesSieve :
+ {ℓcov ℓsie : Level}
+ {c : ob} →
+ (cov : Cover C ℓcov c) →
+ (S : Sieve C ℓsie c) →
+ isProp (coverRefinesSieve cov S)
+ isPropCoverRefinesSieve _ S = isPropΠ (λ _ → isPropPasses S _)
+
+ coverRefinesGeneratedSieve :
+ {ℓ : Level} →
+ {c : ob} →
+ {cov : Cover C ℓ c} →
+ coverRefinesSieve cov (generatedSieve cov)
+ coverRefinesGeneratedSieve i = ∣ i , id , sym (⋆IdL _) ∣₁
+
+ -- The universal property of generatedSieve
+ generatedSieveIsUniversal :
+ {ℓcov ℓsie : Level} →
+ {c : ob} →
+ (cov : Cover C ℓcov c) →
+ (S : Sieve C ℓsie c) →
+ coverRefinesSieve cov S →
+ sieveRefinesSieve (generatedSieve cov) S
+ generatedSieveIsUniversal cov S cov≤S d f =
+ PT.rec (isPropPasses S f) (λ (i , g , eq) →
+ subst (passes S) (sym eq)
+ (closedUnderPrecomposition S g (patchArr cov i) (cov≤S i)) )
+
+ pulledBackSieve :
+ {ℓsie : Level} →
+ {c d : ob} →
+ (Hom[ c , d ]) →
+ Sieve C ℓsie d →
+ Sieve C ℓsie c
+ passes (pulledBackSieve f S) g = passes S (g ⋆ f)
+ isPropPasses (pulledBackSieve f S) g = isPropPasses S _
+ closedUnderPrecomposition (pulledBackSieve f S) p g pass =
+ subst (passes S) (sym (⋆Assoc p g f))
+ (closedUnderPrecomposition S p (g ⋆ f) pass)