open import Cat.Diagram.Colimit.Cocone
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Properties
open import Cat.Instances.Elements
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Diagram.Initial
open import Cat.Prelude

import Cat.Functor.Hom
import Cat.Reasoning

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

open import Cat.Reasoning C
open Cat.Functor.Hom C

open Functor
open _=>_


## 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 and constructing a colimit whose coapex is This involves a clever choice of diagram category: specifically, the category of elements of This may seem like a somewhat odd choice, but recall that the data contained in is the same data as just melted into a soup of points. The colimit we construct will then glue all those points back together into

  coyoneda : is-colimit (γ Fβ Οβ C P) P _
coyoneda = to-is-colimit colim where


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

    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 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 into the coapex of some other cocone 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 and then apply the function we construct to the identity morphism. Naturality follows from the fact that is a cocone, and the components of are natural.

    colim .universal eta _ .Ξ· x px =  eta (elem x px) .Ξ· x id
colim .universal {Q} eta comm .is-natural x y f = funext Ξ» px β
eta (elem y (P.Fβ f px)) .Ξ· y id        β‘Λβ¨ (Ξ» i β comm (induce C P f px) i .Ξ· y id) β©β‘Λ
eta (elem x px) .Ξ· y (f β id)           β‘β¨ ap (eta (elem x px) .Ξ· y) id-comm β©β‘
eta (elem x px) .Ξ· y (id β f)           β‘β¨ happly (eta (elem x px) .is-natural x y f) id β©β‘
Q .Fβ f (eta (elem x px) .Ξ· x id)       β


Next, we need to show that this morphism factors each of the components of 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} eta comm = ext Ξ» x f β
eta (elem x (P.Fβ f (o .section))) .Ξ· x id β‘Λβ¨ (Ξ» i β comm (induce C P f (o .section)) i .Ξ· x id) β©β‘Λ
eta o .Ξ· x (f β id)                        β‘β¨ ap (eta o .Ξ· x) (idr f) β©β‘
eta o .Ξ· x f                               β


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

    colim .unique eta comm Ξ± p = ext Ξ» x px β
Ξ± .Ξ· x px               β‘Λβ¨ ap (Ξ± .Ξ· x) (happly P.F-id px) β©β‘Λ
Ξ± .Ξ· x (P.Fβ id px)     β‘β¨ happly (p _ Ξ·β x) id β©β‘
eta (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 , in that if a pair of natural transformations that agrees on all representables, then all along.

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


The first thing we prove is that any map of presheaves expresses as a cocone over 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 is initial the coslice category under

    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 are two maps such that, for every map with representable domain then 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 can be seen as a βgeneralised elementβ of so that the precondition for can be read as β and agree for all generalised elements with domain any representableβ. The proof is deceptively simple: Since is a colimit, it is an initial object in the category of cocones under The construction Mapβcocone-under lets us express as a cocone under in a way that becomes a cocone homomorphism The condition that agrees with on all generalised elements with representable domains ensures that is also a cocone homomorphism But is initial, so  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 in extend to maps and the functor is fully faithful, two maps in 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 =
ffβ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 _