module Cat.Functor.Hom.Coyoneda {o h} (C : Precategory o h) where

## The Coyoneda lemmaπ

The Coyoneda lemma is, like its dual, a statement about presheaves. It states that βevery presheaf is a colimit of representablesβ, which, in less abstract terms, means that every presheaf arises as some way of gluing together a bunch of (things isomorphic to) hom functors!

module _ (P : Functor (C ^op) (Sets h)) where private module P = Functor P open Element open Element-hom

We start by fixing some presheaf
$P,$
and constructing a colimit whose coapex is
$P.$
This involves a clever choice of diagram category: specifically, the category of elements of
$P.$
This may seem like a somewhat odd choice, but recall that the data
contained in
$β«P$
is the *same* data as
$P,$
just melted into a soup of points. The colimit we construct will then
glue all those points back together into
$P.$

coyoneda : is-colimit (γ Fβ Οβ C P) P _ coyoneda = to-is-colimit colim where

This is done by projecting out of $β«P$ into $C$ via the canonical projection, and then embedding $C$ into the category of presheaves over $C$ via the yoneda embedding. Concretely, what this diagram gives us is a bunch of copies of the hom functor, one for each $px:P(X).$ Then, to construct the injection map, we can just use the (contravariant) functorial action of $P$ to take a $px:P(X)$ and a $f:Hom(A,X)$ to a $P(A).$ This map is natural by functoriality of $P.$

open make-is-colimit module β« = Precategory (β« C P) colim : make-is-colimit (γ Fβ Οβ C P) P colim .Ο x .Ξ· y f = P.Fβ f (x .section) colim .Ο x .is-natural y z f = funext (Ξ» g β happly (P.F-β f g) (x .section)) colim .commutes {x = x} {y = y} f = ext Ξ» z g β P.Fβ (f .hom β g) (y .section) β‘β¨ happly (P.F-β g (f .hom)) (y .section) β©β‘ P.Fβ g (P.Fβ (f .hom) (y .section)) β‘β¨ ap (P.Fβ g) (f .commute) β©β‘ P.Fβ g (x .section) β

Now that weβve constructed a cocone, all that remains is to see that
this is a *colimiting* cocone. Intuitively, it makes sense that
`Reassemble`

should be colimiting:
all weβve done is taken all the data associated with
$P$
and glued it back together. However, proving this does involve futzing
about with various naturality + cocone commuting conditions.

We start by constructing the universal map from $P$ into the coapex of some other cocone $K.$ The components of this natural transformation are obtained in a similar manner to the yoneda lemma; we bundle up the data to construct an object of $β«P,$ and then apply the function we construct to the identity morphism. Naturality follows from the fact that $K$ is a cocone, and the components of $K$ are natural.

colim .universal eps _ .Ξ· x px = eps (elem x px) .Ξ· x id colim .universal {Q} eps comm .is-natural x y f = funext Ξ» px β eps (elem y (P.Fβ f px)) .Ξ· y id β‘Λβ¨ (Ξ» i β comm (induce C P f px) i .Ξ· y id) β©β‘Λ eps (elem x px) .Ξ· y (f β id) β‘β¨ ap (eps (elem x px) .Ξ· y) id-comm β©β‘ eps (elem x px) .Ξ· y (id β f) β‘β¨ happly (eps (elem x px) .is-natural x y f) id β©β‘ Q .Fβ f (eps (elem x px) .Ξ· x id) β

Next, we need to show that this morphism factors each of the
components of
$K.$
The tricky bit of the proof here is that we need to use `induce`

to regard `f`

as a morphism in the category of elements.

colim .factors {o} eps comm = ext Ξ» x f β eps (elem x (P.Fβ f (o .section))) .Ξ· x id β‘Λβ¨ (Ξ» i β comm (induce C P f (o .section)) i .Ξ· x id) β©β‘Λ eps o .Ξ· x (f β id) β‘β¨ ap (eps o .Ξ· x) (idr f) β©β‘ eps o .Ξ· x f β

Finally, uniqueness: This just follows by the commuting conditions on
`Ξ±`

.

colim .unique eps comm Ξ± p = ext Ξ» x px β Ξ± .Ξ· x px β‘Λβ¨ ap (Ξ± .Ξ· x) (happly P.F-id px) β©β‘Λ Ξ± .Ξ· x (P.Fβ id px) β‘β¨ happly (p _ Ξ·β x) id β©β‘ eps (elem x px) .Ξ· x id β

And thatβs it! The important takeaway here is not the shuffling
around of natural transformations required to prove this lemma, but
rather the idea that, unlike Humpty Dumpty, if a presheaf falls off a
wall, we *can* put it back together again.

An important consequence of being able to disassemble presheaves into
colimits of representables is that **representables generate
$PSh(C)$**,
in that if a pair
$f,g$
of natural transformations that agrees on all representables, then
$f=g$
all along.

module _ {Y} (f : P => Y) where private module Y = Functor Y open Cocone

The first thing we prove is that any map
$PβY$
of presheaves expresses
$Y$
as a cocone over
$γ(ΟP).$
The special case `Reassemble`

above
is this procedure for the identity map β whence we see that `coyoneda`

is essentially a
restatement of the fact that
$id$
is initial the coslice category under
$P.$

Mapβcocone-under : Cocone (γ Fβ Οβ C P) Mapβcocone-under .coapex = Y Mapβcocone-under .Ο (elem ob sect) .Ξ· x i = f .Ξ· x (P.β i sect) Mapβcocone-under .Ο (elem ob sect) .is-natural x y h = funext Ξ» a β f .Ξ· _ (P.β (a β h) sect) β‘β¨ happly (f .is-natural _ _ _) _ β©β‘ Y.β (a β h) (f .Ξ· _ sect) β‘β¨ happly (Y.F-β _ _) _ β©β‘ Y.β h (Y.β a (f .Ξ· _ sect)) β‘Λβ¨ ap (Y .Fβ h) (happly (f .is-natural _ _ _) _) β©β‘Λ Y.β h (f .Ξ· _ (P.β a sect)) β Mapβcocone-under .commutes {x} {y} o = ext Ξ» i a β ap (f .Ξ· _) $ P.β (o .hom β a) (y .section) β‘β¨ happly (P.F-β _ _) _ β©β‘ P.β a (P.β (o .hom) (y .section)) β‘β¨ ap (P.Fβ _) (o .commute) β©β‘ P.β a (x .section) β

module _ {X Y : Functor (C ^op) (Sets h)} where private module PSh = Cat.Reasoning (Cat[ C ^op , Sets h ]) module P = Functor X module Y = Functor Y open Cocone-hom open Element open Initial open Cocone

We can now prove that, if $f,g:XβY$ are two maps such that, for every map with representable domain $h:γ(A)βX,$ $fh=gh,$ then $f=g.$ The quantifier structure of this sentence is a bit funky, so watch out for the formalisation below:

Representables-generate-presheaf : {f g : X => Y} β (β {A : Ob} (h : γβ A => X) β f PSh.β h β‘ g PSh.β h) β f β‘ g

A map
$h:γ(A)βX$
can be seen as a βgeneralised elementβ of
$X,$
so that the precondition for
$f=g$
can be read as
β$f$
and
$g$
agree for *all* generalised elements with domain *any*
representableβ. The proof is deceptively simple: Since
$X$
is a colimit, it is an initial object in the category of cocones under
$γ(ΟX).$

The construction `Mapβcocone-under`

lets us
express
$Y$
as a cocone under
$γ(ΟX)$
in a way that
$f$
becomes a cocone homomorphism
$XβY;$
The condition that
$g$
agrees with
$f$
on all generalised elements with representable domains ensures that
$g$
is *also* a cocone homomorphism
$XβY;$
But
$X$
is initial, so
$f=g!$

Representables-generate-presheaf {f} {g} sep = ap hom $ is-contrβis-prop (is-colimitβis-initial-cocone _ (coyoneda X) (Mapβcocone-under X f)) f' g' where f' : Cocone-hom (γ Fβ Οβ C X) _ (Mapβcocone-under X f) f' .hom = f f' .commutes o = trivial! g' : Cocone-hom (γ Fβ Οβ C X) _ (Mapβcocone-under X f) g' .hom = g g' .commutes o = sym $ ext $ unext $ sep $ NT (Ξ» i a β P.β a (o .section)) (Ξ» x y h β ext Ξ» a β P.F-β _ _ # o .section)

An immediate consequence is that, since any pair of maps $f,g:XβY$ in $C$ extend to maps $γ(f),γ(g):γ(X)βγ(Y),$ and the functor $γ(β)$ is fully faithful, two maps in $C$ are equal iff. they agree on all generalised elements:

private module _ where private γ-cancelr : β {X Y : Ob} {f g : Hom X Y} β (β {Z} (h : Hom Z X) β f β h β‘ g β h) β f β‘ g γ-cancelr sep = fully-faithfulβfaithful {F = γ} γ-is-fully-faithful $ Representables-generate-presheaf Ξ» h β ext Ξ» x a β sep (h .Ξ· x a)

However note that we have eliminated a mosquito using a low-orbit ion cannon:

γ-cancelr : β {X Y : Ob} {f g : Hom X Y} β (β {Z} (h : Hom Z X) β f β h β‘ g β h) β f β‘ g γ-cancelr sep = sym (idr _) β sep id β idr _