open import Cat.Functor.Adjoint
open import Cat.Diagram.Sieve
open import Cat.Site.Base hiding (glues)
open import Cat.Prelude

import Cat.Functor.Reasoning.Presheaf as Psh

module Cat.Site.Sheafification where

Sheafification🔗

This module constructs the sheafification of a presheaf on $\mathcal{C}\text{,}$ relative to an arbitrary coverage $J$ on $\mathcal{C}\text{.}$ Abstractly, this is the left adjoint to the inclusion of sheaves on $(\mathcal{C},J)$ into presheaves on $\mathcal{C}\text{:}$ in concrete terms, this means that, given a presheaf $A:\mathrm{PSh}(\mathcal{C})\text{,}$ we construct a $J\text{-sheaf}$ $A^{+}$ and a map $A\to A^{+}$ which is universal among maps from $A$ to sheaves.

Unlike traditional constructions in the literature (e.g. those found in (Johnstone 2002, C2.2.6; Mac Lane and Moerdijk 1994, chaps. V, 3.7; Stacks Project Authors 2018, 7.10)), which construct sheafifications by a two-step construction, working in cubical type theory lets us construct sheafifications all at once, using a higher inductive type. As usual when constructing left adjoints, this boils down to writing down an inductive type with constructors standing for all the “generators” and “relations” that the object must satisfy, then a bit of plumbing to establish the universal property in categorical terms.

module Sheafification {o ℓ ℓc} {C : Precategory o ℓ} (J : Coverage C ℓc) {ℓs} (A : Functor (C ^op) (Sets ℓs)) where
  open Precategory C
  open Functor

  private
    module A = Functor A
    variable
      U V W : ⌞ C ⌟
      f g h : Hom U V

  -- The constructors 'glue' and 'glues' are why we define pre.Parts and
  -- pre.is-patch for "non-functors" (freestanding actions).
  --
  -- Ideally we would like to define Sheafify and Sheafify₀ by mutual
  -- recursion so we could instead say Patch Sheafify (J .cover c) but
  -- this angers both the termination and the positivity checker (and
  -- occasionally the scope checker).

While this construction might not be familiar to working mathematicians, we will see by, investigating each constructor in turn, that there is a very natural set of “generators” and “relations” that present the sheafification. Let us start with the generators: how can you construct an element of $A^{+}(U)\text{?}$

First, $A^{+}$ admits a (universal) natural transformation from $A\text{,}$ so we must have a constructor standing for that, namely inc. Second, $A^{+}$ must be a functor, so given $x:A^{+}(U)$ and $f:\mathcal{C}(V,U)\text{,}$ we have a constructor map standing for the restriction $A^{+}(f)(x):A^{+}(V)\text{.}$ Finally, $A^{+}$ is a sheaf, so given any $J\text{-covering}$ sieve $s\in J(U)\text{,}$ we can glue together a patch with respect to $s\text{,}$ living in $A^{+}(U)\text{.}$

  data Sheafify₀ : ⌞ C ⌟ → Type (o ⊔ ℓ ⊔ ℓs ⊔ ℓc) where
    inc : A ʻ U → Sheafify₀ U

    map : (f : Hom U V) → Sheafify₀ V → Sheafify₀ U

    glue
      : (c : J .covers U) (p : pre.Parts C map (J .cover c))
      → (g : pre.is-patch C map (J .cover c) p)
      → Sheafify₀ U

Then, we come to the relations, which are defined as path constructors. First, we have constructors assuring that map is functorial, and that inc is a natural transformation:

    map-id : ∀ x → map {U = U} id x ≡ x
    map-∘  : ∀ x → map (g ∘ f) x ≡ map f (map g x)

    inc-natural : (x : A ʻ U) → inc (A ⟪ f ⟫ x) ≡ map f (inc x)

To ensure that $A^{+}$ is a sheaf, we have two constructors: one states that $A^{+}$ is separated for any $J\text{-covering}$ sieve, and one states that the point obtained by glue really is a section of the given patch.

    sep
      : ∀ {x y : Sheafify₀ U} (c : J .covers U)
      → (l : ∀ {V} (f : Hom V U) (hf : f ∈ J .cover c) → map f x ≡ map f y)
      → x ≡ y

    glues
      : (c : J .covers U) (p : pre.Parts C map (J .cover c))
      → (g : pre.is-patch C map (J .cover c) p)
      → pre.is-section C map (J .cover c) (glue c p g) p

Finally, we must tame all these generators for equality, by truncating $A^{+}(U)$ to a set.

    squash : is-set (Sheafify₀ U)

By distributing the data above, we see that $A^{+}$ is indeed a functor (Sheafify), that it is separated, and that it is a sheaf.

  Sheafify : Functor (C ^op) (Sets (o ⊔ ℓ ⊔ ℓs ⊔ ℓc))
  Sheafify .F₀ x .∣_∣ = Sheafify₀ x
  Sheafify .F₀ x .is-tr = squash
  Sheafify .F₁ = map
  Sheafify .F-id    = funext map-id
  Sheafify .F-∘ f g = funext map-∘

  Sheafify-is-sep : is-separated J Sheafify
  Sheafify-is-sep c = sep c

  Sheafify-is-sheaf : is-sheaf J Sheafify
  Sheafify-is-sheaf = from-is-separated Sheafify-is-sep λ c s → record
    { whole = glue c (s .part) (s .patch)
    ; glues = glues c (s .part) (s .patch)
    }

An induction principle🔗

It remains to prove the universal property of $A^{+}\text{.}$ Showing existence of the natural transformation $A^{+}$ is easy, and showing that we can factors maps $A\to B$ through $A^{+}$ when $B$ is a sheaf is similarly uncomplicated. However, showing uniqueness of this factorisation is slightly more complicated: we will need an induction principle for $A^{+}$ to tackle this problem in a sensible way.

Every higher-inductive type has a mechanically derivable eliminator into propositions, which lets us get a section of a proposition $P$ given only its values at the point constructor. But sheafifications have three point constructors: inc, map, and glue. Showing a proposition is preserved by map feels redundant, since functoriality feels like it should be automatic, and having to handle the glue constructor feels unnatural.

Hutzler shows us how to give a more natural elimination principle, which furthermore handles map automatically. We will assume that we have a family of propositions $P\text{,}$ with sections over inc:

  Sheafify-elim-prop
    : ∀ {ℓp} (P : ∀ {U} → Sheafify₀ U → Type ℓp)
    → (pprop : ∀ {U} (x : Sheafify₀ U) → is-prop (P x))
    → (pinc : ∀ {U : ⌞ C ⌟} (x : A ʻ U) → P (inc x))

Instead of asking for $P$ over glue, we will ask instead that $P$ be local for any $J\text{-covering}$ sieve. Explicitly, this means that we need to show $P(x)\text{,}$ for $x:A^{+}(U)$ and a $J\text{-covering}$ sieve $s\text{;}$ but we’re allowed to assume that $P$ has already been shown for any restriction $A^{+}(f)(x)\text{,}$ as long as $f\in s\text{.}$

    → (plocal
        : ∀ {U : ⌞ C ⌟} (c : J .covers U) (x : Sheafify₀ U)
        → (∀ {V} (f : Hom V U) (hf : f ∈ J .cover c) → P (map f x)) → P x)
    → ∀ {U} (x : Sheafify₀ U) → P x

The key idea is to strengthen $P(x)$ to the proposition “$P$ holds at every restriction of $x$”; we will call this stronger proposition $P^{\prime }\text{.}$ Since $x$ is its own restriction along the identity, it is clear that $P^{\prime }(x)$ implies $P(x)\text{;}$ it is also automatic that $P^{\prime }$ is a family of propositions as well.

  Sheafify-elim-prop {ℓp} P pprop pinc plocal x = unp' (go x) where opaque
    P' : ∀ {U} (x : Sheafify₀ U) → Type (o ⊔ ℓ ⊔ ℓp)
    P' {U} x = ∀ {V} (f : Hom V U) → P (map f x)

    unp' : ∀ {U} {x : Sheafify₀ U} → P' x → P x
    unp' p' = subst P (map-id _) (p' id)

    p'prp : ∀ {U} (x : Sheafify₀ U) → is-prop (P' x)
    p'prp x = Π-is-hlevel'  λ V → Π-is-hlevel  λ f → pprop (map f x)

We now turn to showing $P^{\prime }$ over every point constructor. First, it is preserved by map, by functoriality: in a bit more detail, suppose we have $x:A^{+}(V)\text{,}$ $f:\mathcal{C}(U,V)\text{,}$ and $P^{\prime }(x)\text{;}$ we want to show $P^{\prime }(A^{+}(f)(x))\text{.}$ Unfolding the definition of $P^{\prime }\text{,}$ this means that we must show $P(A^{+}(g)(A^{+}(f)(x)))\text{,}$ for any $g:\mathcal{C}(W,V)\text{;}$ but our assumption means that we have $P(A^{+}(h)(x))$ for any $h:\mathcal{C}(-,V)\text{.}$ Taking $h=fg$ gives $P(A^{+}(fg)(x))\text{,}$ which is equal to our goal by functoriality.

    p'map : ∀ {U V : ⌞ C ⌟} (f : Hom U V) (x : Sheafify₀ V) → P' x → P' (map f x)
    p'map f x p g = subst P (map-∘ _) (p (f ∘ g))

Similarly, we can show $P^{\prime }(x)$ for the inclusion of an $x:A(U)$ at every restriction, by naturality of inc.

    p'inc : ∀ {U : ⌞ C ⌟} (x : A ʻ U) → P' (inc x)
    p'inc x {V} f = subst P (inc-natural x) (pinc (A ⟪ f ⟫ x))

Finally, we must show that $P^{\prime }$ preserves the glue constructor. This is a bit more involved: suppose we have a $J\text{-covering}$ sieve $s$ on $U\text{,}$ and a patch $p$ over $s\text{.}$ For our induction hypothesis, we assume $P^{\prime }(p(f))$ for any $f\in s\text{.}$ We want to show $P(A^{+}(f)(\mathrm{glue}p))\text{,}$ given any $f:\mathcal{C}(U,V)\text{.}$

    p'glue
      : ∀ {U : ⌞ C ⌟} (c : J .covers U) (p : pre.Parts C map (J .cover c))
      → (g : pre.is-patch C map (J .cover c) p)
      → (∀ {V} (f : Hom V U) (hf : f ∈ J .cover c) → P' (p f hf))
      → P' (glue c p g)

We will use the assumption that $P$ is local, at the pullback sieve $f^{\ast }(s)\text{,}$ which is $J\text{-covering}$ since $J$ is a site: to show $P(A^{+}(f)(\mathrm{glue}p))\text{,}$ it will suffice to show this at every restriction along $g\in f^{\ast }(s)\text{.}$ Since $\mathrm{glue}p$ is a section of $p\text{,}$ it becomes equal to $p(fg)$ after restricting along such a $g\text{.}$ We have $P(p(fg))$ by assumption, and $P(A^{+}(fg)(\mathrm{glue}p))$ by the preceding observation, so we can finish by functoriality. This is a slightly tricky argument, so the formalisation may actually be easier to read:

    p'glue c p compat loc f = ∥-∥-out (pprop _) do
      (c' , sub) ← J .stable c f
      pure $ plocal c' (map f (glue c p compat)) λ g hg →
        let
          it : P (map id (p (f ∘ g) (sub g hg)))
          it = loc (f ∘ g) (sub g hg) id
          q = map id (p (f ∘ g) _)            ≡⟨ map-id _ ⟩≡
              p (f ∘ g) _                     ≡˘⟨ glues c p compat (f ∘ g) (sub g hg) ⟩≡˘
              map (f ∘ g) (glue c p compat)   ≡⟨ map-∘ _ ⟩≡
              map g (map f (glue c p compat)) ∎
        in subst P q it

    go : ∀ {U} (x : Sheafify₀ U) → P' x
    go (map f x) = p'map f x (go x)
    go (inc x)   = p'inc x
    go (glue c p g) = p'glue c p g λ f hf → go (p f hf)
    go (inc-natural {f = f} x i) = is-prop→pathp (λ i → p'prp (inc-natural x i)) (p'inc (A.₁ f x)) (p'map f (inc x) (p'inc x)) i
    go (sep {x = x} {y = y} c l i) = is-prop→pathp (λ i → p'prp (sep c l i)) (go x) (go y) i
    go (map-id x i) = is-prop→pathp (λ i → p'prp (map-id x i)) (p'map id x (go x)) (go x) i
    go (map-∘ {g = g} {f = f} x i) = is-prop→pathp (λ i → p'prp (map-∘ x i)) (p'map (g ∘ f) x (go x)) (p'map f (map g x) (p'map g x (go x))) i
    go (glues c p g f hf i) = is-prop→pathp (λ i → p'prp (glues c p g f hf i)) (p'map f (glue c p g) (p'glue c p g λ g hg → go (p g hg))) (go (p f hf)) i
    go (squash x y p q i j) = is-prop→squarep (λ i j → p'prp (squash x y p q i j)) (λ i → go x) (λ i → go (p i)) (λ i → go (q i)) (λ i → go y) i j

The universal property🔗

module Small {ℓ} {C : Precategory ℓ ℓ} (J : Coverage C ℓ)  where
  open Sheafification J

  open _=>_

  private variable A : Functor (C ^op) (Sets ℓ)

Using the induction principle above, we may show the categorical universal property of $A^{+}\text{.}$ However, at this stage, we must pay attention to the universe levels involved. Let us recap:

• A site, as a category $\mathcal{C}$ with a coverage $J\text{,}$ is parametrised over three universe levels: one for the type of objects of $\mathcal{C}\text{,}$ one for $\mathcal{C}\text{’s}$ $\mathbf{Hom}\text{-sets,}$ and one for the collection of $J\text{-covers.}$ Finally, we can consider presheaves on $\mathcal{C}$ valued in a completely arbitrary universe.

  The sheafification construction is fully general: the type $A^{+}(U)$ simply lives in the least universe larger than all those that parametrise $\mathcal{C}\text{,}$ $J$ and $A\text{.}$

• The functor category $[{\mathcal{C}}^{\mathrm{op}},{\mathbf{Sets}}_{\ell }]$ is parametrised by a universe level $\ell \text{.}$ Among other things, this means that we can only really consider natural transformations between presheaves valued in the same universe level.

  Moreover, to get a Cartesian closed category of presheaves, $\mathcal{C}$ must be small — its objects and $\mathbf{Hom}\text{s}$ must live in the same universe — and they must be valued in that same universe level.

In practice, this means that, while the construction of $A^{+}(U)$ is parametrised over four universe levels, we only obtain a nice universal property if $\mathcal{C}$ is some $\ell \text{-small}$ category, equipped with an $\ell \text{-small}$ coverage, and we are talking about presheaves valued in the category ${\mathbf{Sets}}_{\ell }$ of $\ell \text{-small}$ sets. As a result, the sheafification functor qua left adjoint is only parametrised over this one universe level.

Returning to the construction, the universal natural transformation is easy to define:

  unit : A => Sheafify A
  unit .η _ = inc
  unit .is-natural x y f = funext inc-natural

And, if $B$ is a $J\text{-sheaf,}$ extending a map $\eta :A\to B$ to a map ${\eta }^{\prime }:A^{+}\to B$ is similarly straightforward. At each construction of $A^{+}(U)\text{,}$ we have a corresponding operation valued in $B(U)\text{,}$ deferring to $\eta$ for the inclusion of points from $A(U)\text{.}$ Similarly, the path constructors are all handled by the corresponding laws in $B\text{.}$

  univ : (B : Functor (C ^op) (Sets ℓ)) → is-sheaf J B → A => B → Sheafify A => B
  univ {A = A} G shf eta = nt where
    private module G = Psh G
    go : ∀ U → Sheafify₀ A U → G ʻ U
    go U (inc x)   = eta .η U x
    go U (map f x) = G ⟪ f ⟫ (go _ x)
    go U (glue c p g) =
      shf .whole c record { patch = λ f hf h hhf i → go _ (g f hf h hhf i) }

    go U (map-id x i) = G.F-id {x = go _ x} i
    go U (map-∘ {g = g} {f = f} x i) = G.F-∘ f g {x = go _ x} i
    go U (inc-natural {f = f} x i) = eta .is-natural _ U f i x
    go U (sep {x = x} {y = y} c l i) = shf .separate c {go _ x} {go _ y} (λ f hf i → go _ (l f hf i)) i
    go U (glues c p g f hf i) = shf .is-sheaf.glues c record { patch = λ f hf h hhf i → go _ (g f hf h hhf i) } f hf i
    go U (squash x y p q i j) = G.₀ U .is-tr (go U x) (go U y) (λ i → go U (p i)) (λ i → go U (q i)) i j

    nt : Sheafify A => G
    nt .η = go
    nt .is-natural x y f = refl

Finally, we can show that ${\eta }^{\prime }$ is the unique map which extends $\eta \text{.}$ This is very straightforward with our induction principle for $A^{+}\text{,}$ and the assumption that $B$ is a $J\text{-sheaf}$ implies that equality in $B(U)$ is $J\text{-local.}$

  unique
    : (G : Functor (C ^op) (Sets ℓ)) (shf : is-sheaf J G) (eta : A => G) (eps : Sheafify A => G)
    → (∀ U (x : A ʻ U) → eps .η U (inc x) ≡ eta .η U x)
    → univ G shf eta ≡ eps
  unique {A = A} G shf eta eps comm = ext λ i → Sheafify-elim-prop A
    (λ {v} x → univ G shf eta .η v x ≡ eps .η v x)
    (λ {U} x → hlevel )
    (λ x → sym (comm _ x))
    (λ c x l → is-sheaf.separate shf c (λ f hf → l f hf ∙ eps .is-natural _ _ _ # _))

  private module fo = Free-object

  make-free-sheaf : ∀ F → Free-object (forget-sheaf J ℓ) F
  make-free-sheaf F .fo.free = Sheafify F , Sheafify-is-sheaf F
  make-free-sheaf F .fo.unit = unit
  make-free-sheaf F .fo.fold {G , shf} = univ G shf
  make-free-sheaf F .fo.commute = trivial!
  make-free-sheaf F .fo.unique {G , shf} _ p = sym $
    unique G shf _ _ λ U x → p ηₚ _ $ₚ _