module Cat.Site.Sheafification where

# Sheafification🔗

The higher-inductive construction of sheafification presented in this
module is originally due to Matthias Hutzler, in code that
was contributed
to the `cubical`

library. The `cubical`

library is distributed under the terms of the MIT license, available
here.

This module constructs the **sheafification** of a
presheaf on
$C,$
relative to an arbitrary coverage
$J$
on
$C.$
Abstractly, this is the left adjoint to the
inclusion of sheaves on
$(C,J)$
into presheaves on
$C:$
in concrete terms, this means that, given a presheaf
$A:PSh(C),$
we construct a
$J-sheaf$
$A_{+}$
and a map
$A→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)?$

First,
$A_{+}$
admits a (universal) natural transformation from
$A,$
so we must have a constructor standing for that, namely `inc`

. Second,
$A_{+}$
must be a functor, so given
$x:A_{+}(U)$
and
$f:C(V,U),$
we have a constructor `map`

standing for
the restriction
$A_{+}(f)(x):A_{+}(V).$
Finally,
$A_{+}$
is a sheaf, so
given any
$J-covering$
sieve
$s∈J(U),$
we can `glue`

together a patch with
respect to
$s,$
living in
$A_{+}(U).$

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-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_{+}.$
Showing existence of the natural transformation
$A_{+}$
is easy, and showing that we can factors maps
$A→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,$
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-covering$
sieve. Explicitly, this means that we need to show
$P(x),$
for
$x:A_{+}(U)$
and a
$J-covering$
sieve
$s;$
but we’re allowed to assume that
$P$
has already been shown for any restriction
$A_{+}(f)(x),$
as long as
$f∈s.$

→ (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_{′}.$ Since $x$ is its own restriction along the identity, it is clear that $P_{′}(x)$ implies $P(x);$ it is also automatic that $P_{′}$ 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' 1 λ V → Π-is-hlevel 1 λ f → pprop (map f x)

We now turn to showing
$P_{′}$
over every point constructor. First, it is preserved by `map`

, by
functoriality: in a bit more detail, suppose we have
$x:A_{+}(V),$
$f:C(U,V),$
and
$P_{′}(x);$
we want to show
$P_{′}(A_{+}(f)(x)).$
Unfolding the definition of
$P_{′},$
this means that we must show
$P(A_{+}(g)(A_{+}(f)(x))),$
for any
$g:C(W,V);$
but our assumption means that we have
$P(A_{+}(h)(x))$
for any
$h:C(−,V).$
Taking
$h=fg$
gives
$P(A_{+}(fg)(x)),$
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_{′}(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_{′}$
preserves the `glue`

constructor.
This is a bit more involved: suppose we have a
$J-covering$
sieve
$s$
on
$U,$
and a patch
$p$
over
$s.$
For our induction hypothesis, we assume
$P_{′}(p(f))$
for any
$f∈s.$
We want to show
$P(A_{+}(f)(gluep)),$
given any
$f:C(U,V).$

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_{∗}(s),$ which is $J-covering$ since $J$ is a site: to show $P(A_{+}(f)(gluep)),$ it will suffice to show this at every restriction along $g∈f_{∗}(s).$ Since $gluep$ is a section of $p,$ it becomes equal to $p(fg)$ after restricting along such a $g.$ We have $P(p(fg))$ by assumption, and $P(A_{+}(fg)(gluep))$ 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_{+}.$ However, at this stage, we must pay attention to the universe levels involved. Let us recap:

A site, as a category $C$ with a coverage $J,$ is parametrised over three universe levels: one for the type of objects of $C,$ one for $C’s$ $Hom-sets,$ and one for the collection of $J-covers.$ Finally, we can consider presheaves on $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 $C,$ $J$ and $A.$

The functor category $[C_{op},Sets_{ℓ}]$ is parametrised by a universe level $ℓ.$ 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, $C$ must be small — its objects and $Homs$ 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
$C$
is some
$ℓ-small$
category, equipped with an
$ℓ-small$
coverage, and we are talking about presheaves valued in the category
$Sets_{ℓ}$
of
$ℓ-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-sheaf,$ extending a map $η:A→B$ to a map $η_{′}:A_{+}→B$ is similarly straightforward. At each construction of $A_{+}(U),$ we have a corresponding operation valued in $B(U),$ deferring to $η$ for the inclusion of points from $A(U).$ Similarly, the path constructors are all handled by the corresponding laws in $B.$

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

##
We will leave the laws in this little `<details>`

block, since they’re a tad uglier than the cases above. Note also that
naturality of
$η_{′}$
is a definitional equality.

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 $η_{′}$ is the unique map which extends $η.$ This is very straightforward with our induction principle for $A_{+},$ and the assumption that $B$ is a $J-sheaf$ implies that equality in $B(U)$ is $J-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 1) (λ 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 ηₚ _ $ₚ _

## References

- Johnstone, Peter T. 2002.
*Sketches of an Elephant: a Topos Theory Compendium*. Oxford Logic Guides. New York, NY: Oxford Univ. Press. https://cds.cern.ch/record/592033. - Mac Lane, Saunders, and Ieke Moerdijk. 1994.
*Sheaves in Geometry and Logic: A First Introduction to Topos Theory*. Universitext. New York, NY: Springer New York. https://doi.org/10.1007/978-1-4612-0927-0. - Stacks Project Authors, The. 2018. “
*Stacks Project*.” https://stacks.math.columbia.edu.