Sites, sheaves and sheafification as a QIT (#1031)

* 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

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

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

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)

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

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