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

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 _