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 El C P
  open Element
  open Element-hom

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

  coyoneda : is-colimit (γ‚ˆ F∘ Ο€β‚š) P _
  coyoneda = to-is-colimit colim where

This is done by projecting out of ∫P\int P into C\mathcal{C} via the canonical projection, and then embedding C\mathcal{C} into the category of presheaves over C\mathcal{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)px : P(X). Then, to construct the injection map, we can just use the (contravariant) functorial action of PP to take a px:P(X)px : P(X) and a f:Hom(A,X)f : Hom(A, X) to a P(A)P(A). This map is natural by functoriality of PP.

    open make-is-colimit
    module ∫ = Precategory ∫

    colim : make-is-colimit (γ‚ˆ F∘ Ο€β‚š) 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 =
      Nat-path Ξ» z β†’ funext Ξ» 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 PP 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 PP into the coapex of some other cocone KK. 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\int P, and then apply the function we construct to the identity morphism. Naturality follows from the fact that KK is a cocone, and the components of KK 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 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 βŸ©β‰‘
      F₁ Q f (eps (elem x px) .Ξ· x id) ∎

Next, we need to show that this morphism factors each of the components of KK. 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 = Nat-path Ξ» x β†’ funext Ξ» f β†’
      eps (elem x (P.F₁ f (o .section))) .Ξ· x id β‰‘Λ˜βŸ¨ (Ξ» i β†’ comm (induce 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 = Nat-path Ξ» x β†’ funext Ξ» 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)\mathrm{PSh}(C), in that if a pair f,gf, g of natural transformations that agrees on all representables, then f=gf = 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β‡’YP \Rightarrow Y of presheaves expresses YY as a cocone over γ‚ˆ(Ο€P)γ‚ˆ (\pi 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\mathrm{id}_{} is initial the coslice category under PP.

    Mapβ†’cocone-under : Cocone (γ‚ˆ F∘ Ο€β‚š)
    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 = Nat-path λ i → funext λ 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 f,g:Xβ‡’Yf, g : X \Rightarrow Y are two maps such that, for every map with representable domain h:γ‚ˆ(A)β†’Xh : γ‚ˆ(A) \to X, fh=ghfh = gh, then f=gf = 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)β‡’Xh : γ‚ˆ(A) \Rightarrow X can be seen as a β€œgeneralised element” of XX, so that the precondition for f=gf = g can be read as β€œff and gg agree for all generalised elements with domain any representable”. The proof is deceptively simple: Since XX is a colimit, it is an initial object in the category of cocones under γ‚ˆ(Ο€X)γ‚ˆ (\pi X).

The construction Mapβ†’cocone-under lets us express YY as a cocone under γ‚ˆ(Ο€X)γ‚ˆ (\pi X) in a way that ff becomes a cocone homomorphism Xβ†’YX \to Y; The condition that gg agrees with ff on all generalised elements with representable domains ensures that gg is also a cocone homomorphism Xβ†’YX \to Y; But XX is initial, so f=gf = 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∘ El.Ο€β‚š C X) _ (Mapβ†’cocone-under X f)
      fβ€² .hom = f
      fβ€² .commutes o = Nat-path (Ξ» _ β†’ refl)

      gβ€² : Cocone-hom (γ‚ˆ F∘ El.Ο€β‚š C X) _ (Mapβ†’cocone-under X f)
      gβ€² .hom = g
      gβ€² .commutes o = Nat-path Ξ» x β†’ sym (sep $
        NT (Ξ» i a β†’ P.₁ a (o .section)) Ξ» x y h β†’
          funext Ξ» a β†’ P.F-∘ _ _ $β‚š o .section) Ξ·β‚š x

An immediate consequence is that, since any pair of maps f,g:Xβ†’Yf, g : X \to Y in C\mathcal{C} extend to maps γ‚ˆ(f),γ‚ˆ(g):γ‚ˆ(X)β†’γ‚ˆ(Y)γ‚ˆ(f), γ‚ˆ(g) : γ‚ˆ(X) \to γ‚ˆ(Y), and the functor γ‚ˆ(βˆ’)γ‚ˆ(-) is fully faithful, two maps in C\mathcal{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 β†’ Nat-path Ξ» x β†’ funext Ξ» 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 _