module Cat.Site.Instances.Canonical {o β} (C : Precategory o β) where

# The canonical coverageπ

Every sieve
$S$
on an object
$U$
(in a category
$C)$
may be regarded as a *diagram* in
$C,$
by first interpreting it
as a presheaf, then considering the projection functor

with domain the category of elements of $S;$ The objects of this category consist of triples $i:C,$ $f:iβU,$ and a (propositional) witness that $fβS.$ Thus, purely formally, the object $U$ is the nadir of a cocone under $S-qua-diagram,$ since we can give the component of a natural transformation $ΟβU$ by projecting the arrow.

sieveβcocone : β {U} (S : Sieve C U) β Οβ C (to-presheaf S) => Const U sieveβcocone S .Ξ· (elem i (f , fβS)) = f sieveβcocone S .is-natural (elem _ (f , _)) (elem _ (g , _)) h = g β h .hom β‘β¨ ap fst (h .commute) β©β‘ f β‘β¨ introl refl β©β‘ id β f β

Thus, under this setup, a natural question to ask about *any*
sieve is whether it forms a colimit diagram. This
is also a notion of *covering*, which we can impose on any
category, since *any* given colimit diagram with nadir
$U$
can be seen as a covering of
$U$
by the objects in
$S,$
which sit inside according to the *maps* in
$S.$
Johnstone (2002,
C2.2.8) refers to the sieves which *are* colimiting
cocones as βeffective-epimorphicβ. We will instead follow Lester (2019)
and refer to them as **colim sieves**.

is-colim : β {U} β Sieve C U β Type _ is-colim {U} S = is-colimit _ U (sieveβcocone S)

Natural though it is, unfortunately, being a colim sieve is
*not* a property we can ask of sieves to get a site. The reason is that,
in an arbitrary category, colimits may not be preserved by pullback; in terms of
sieves, even if
$S$
is a colim sieve over
$U,$
we may not have that
$f_{β}(S)$
is a colim sieve over
$V$
for
$f:VβU.$
We can, however, turn this into a site, by restricting the notion of
colim sieve so that itβs stable under pullbacks: we say that
$S$
is a **universal
colim sieve** if
$f_{β}(S)$
is a colim sieve, for any appropriate
$f.$

is-universal-colim : β {U} β Sieve C U β Type _ is-universal-colim {U} S = β {V} (f : Hom V U) β is-colim (pullback f S)

Since this is a pullback-stable property of sieves, we can get a
site. We refer to this as the **canonical coverage** on a
category
$C.$

abstract is-universal-colim-is-stable : β {U V} (f : Hom V U) (S : Sieve C U) β is-universal-colim S β is-universal-colim (pullback f S) is-universal-colim-is-stable f S hS g = subst is-colim pullback-β (hS (f β g)) is-universal-colimβis-colim : β {U} (S : Sieve C U) β is-universal-colim S β is-colim S is-universal-colimβis-colim S u = subst is-colim pullback-id (u id) Canonical-coverage : Coverage C (o β β) Canonical-coverage = from-stable-property is-universal-colim is-universal-colim-is-stable

## Representables as sheavesπ

We will now investigate the matter of sheaves for the canonical topology. First, let $S$ be an arbitrary sieve on $U:C,$ and suppose that we have a patch $p$ for $C(β,V)$ over $S:$ this means that we have a function $p(f):WβV,$ for $f$ a map $WβU$ belonging to $S.$ Since the components of a cocone under $S$ are indexed precisely by these maps, we see that $p(β)$ is a transformation $SβConstV.$

patchβcocone : β {U V} (S : Sieve C U) β Patch (Hom-into C V) S β Οβ C (to-presheaf S) => !Const V Fβ !F patchβcocone S p .Ξ· (elem _ (f , hf)) = p .part f hf

It remains to show that this transformation is natural. We compute:

patchβcocone S p .is-natural (elem _ (f , hf)) (elem _ (g , hg)) h = p .part g hg β h .hom β‘β¨ p .patch g hg (h .hom) (S .closed hg (h .hom)) β©β‘ p .part (g β h .hom) _ β‘β¨ app p (ap fst (h .commute)) β©β‘ p .part f _ β‘β¨ introl refl β©β‘ id β p .part f _ β

Now suppose that $S$ is not just a sieve, but a colim sieve, as defined above. Since any patch $p$ for $C(β,V)$ gives a cocone under $S$ with nadir $V,$ and $U$ is the colimit of $S,$ we have a map $Ο:UβV$ which satisfies $Οβf=p(f),$ for any $fβS.$

is-colimβγ-is-sheaf : β {U V} (S : Sieve C U) β is-colim S β is-sheafβ (Hom-into C V) S is-colimβγ-is-sheaf {U} {V} S colim p = uniq where module x = is-lan colim p' : Οβ C (to-presheaf S) => !Const V Fβ !F p' = patchβcocone S p

Note now that $Ο,$ with its βcomputation ruleβ, is precisely a section for the patch $p.$

Ο : Hom U V Ο = x.Ο p' .Ξ· tt ΟΞ² : β {W} (f : Hom W _) hf β Ο β f β‘ p .part f hf ΟΞ² f hf = x.Ο-comm {Ξ± = p'} Ξ·β elem _ (f , hf) β app p refl

But `Ο`

is not just *a* map with this property; it
is *the unique* map with this property. Since sections of
$p$
correspond precisely to this data, we have that
$C(β,V)$
is a sheaf for
$S,$
as soon as
$S$
is a colim sieve.

uniq : is-contr (Section _ p) uniq .centre = record { glues = ΟΞ² } uniq .paths x = ext $ x.Ο-uniq {Ο' = !constβΏ _} (ext Ξ» i β sym (x .glues _ _)) Ξ·β tt

Generalising the proof above, we conclude that *any*
representable functor
$C(β,U)$
is a sheaf for the canonical coverage.

γ-is-sheaf-canonical : β {U} β is-sheaf Canonical-coverage (Hom-into C U) γ-is-sheaf-canonical = from-is-sheafβ Ξ» (S , hS) β is-colimβγ-is-sheaf S (is-universal-colimβis-colim S hS)

## Subcanonical coveragesπ

We can now ask: is there a converse to this result, i.e., if every
$C(β,U)$
is a sheaf for a coverage
$J,$
must it be the canonical coverage? The answer is *not quite*,
since that is too strong. But we *can* show that all the sieves
in
$J$
are universal colim sieves! We will refer to any coverage
$J$
which satisfies the following equivalent conditions as a
**subcanonical coverage**:

- Every representable functor $C(β,U)$ is a sheaf for $J;$
- Every covering sieve in $J$ is universally colimiting.

is-subcanonical : β {βc} β Coverage C βc β Type _ is-subcanonical J = β {U} (S : J .covers U) β is-universal-colim (J .cover S)

make-is-colim : β {U} (S : Sieve C U) β Type _ make-is-colim {U} S = make-is-colimit (Οβ C (to-presheaf S)) U is-subcanonicalβγ-is-sheaf : β {βc} (J : Coverage C βc) β is-subcanonical J β β {V} β is-sheaf J (Hom-into C V) is-subcanonicalβγ-is-sheaf J sub {V} = from-is-sheafβ Ξ» c β is-colimβγ-is-sheaf _ (is-universal-colimβis-colim (J .cover c) (sub _))

For concreteness, we formalise the statement β$J$ is a subcanonical coverageβ as property (2); We must then show that $J$ is subcanonical if every representable is a $J-sheaf.$

γ-is-sheafβis-subcanonical : β {βc} (J : Coverage C βc) β (β {V} β is-sheaf J (Hom-into C V)) β is-subcanonical J γ-is-sheafβis-subcanonical J shf {U} S {V} f = to-is-colimitp mk refl where open make-is-colimit

So, suppose we have such a $J,$ a covering sieve $S:J(U),$ and a map $f:VβU.$ We want to show that $V$ is the colimit of $f_{β}(S).$ First, we get the cocone $Ο_{S}βConstU$ out of the way: this is as, as weβve seen repeatedly, projecting the arrow.

mk : make-is-colim (pullback f (J .cover S)) mk .Ο (elem V' (g , hg)) = g mk .commutes f = ap fst (f .commute)

Now for the interesting part, universality. Our inputs are an object $W,$ and a function $Ξ΅$ which, given a map $g:XβV$ in $f_{β}(S)$ (i.e., such that $fgβS),$ produces $Ξ΅(g):XβW.$ Moreover, if we have some $h:YβX$ with $fghβS,$ then $Ξ΅$ satisfies $Ξ΅(g)βh=Ξ΅(gh).$ What we want is, initially, a map $VβW.$ But note that $Ξ΅(β)$ is precisely the data of a patch for $C(β,W)$ under $f_{β}(S)!$

mk .universal {W} Ξ΅ comm = [_] .centre .whole module univ where Ξ΅' : Patch (γβ C W) (pullback f (J .cover S)) Ξ΅' .part g hg = Ξ΅ (elem _ (_ , hg)) Ξ΅' .patch g hg h hhg = comm (elem-hom h (Ξ£-prop-path! refl))

Since
$C(β,W)$
was assumed to be a sheaf for
$S,$
itβs also a sheaf for any pullback of
$S,$
including
$f_{β}(S);$
The patch induced by
$Ξ΅$
thus glues to a unique *section*, which we will write
$[Ξ΅].$
What does this section consist of? Well, first, since
$f_{β}(S)$
covers
$V,$
a map
$VβW,$
like we wanted; It also contains evidence that, for
$g:WβV$
belonging to
$f_{β}(S),$
we have
$[Ξ΅]βg=Ξ΅(g).$

[_] : is-contr (Section (Hom-into C W) Ξ΅') [_] = is-sheaf-pullback shf S f Ξ΅' mk .factors {elem W (g , hg)} Ξ΅ p = univ.[ Ξ΅ ] p .centre .glues _ _

Finally, for
$V$
to be a colimit, we must show uniqueness of the map
$[Ξ΅]:VβW,$
in the sense that if we have
$Ο:VβW$
which *also* satisfies
$Οβf=Ξ΅(f)$
for any
$fβS,$
then we must have
$[Ξ΅]=Ο.$
But note that this commutativity condition is precisely what it means
for
$Ο$
to underlie a section for
$Ξ΅-qua-patch;$
so since
$C(β,W)$
is a sheaf, this
$Ο$
must be equal to the
$[Ξ΅]$
we obtained from *the* section for
$Ξ΅.$

mk .unique Ξ΅ p Ο q = sym $ ap whole $ univ.[ Ξ΅ ] p .paths record { glues = Ξ» f hf β q (elem _ (f , hf)) }

## 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. - Lester, Cynthia. 2019. βCovers in the Canonical Grothendieck Topology.β https://arxiv.org/abs/1909.03384.