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

  coyoneda : is-colimit (よ F∘ πₚ C P) P _
  coyoneda = to-is-colimit colim where

This is done by projecting out of $\int P$ into $\mathcal{C}$ via the canonical projection, and then embedding $\mathcal{C}$ into the category of presheaves over $\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)\text{.}$ 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)\text{.}$ This map is natural by functoriality of $P\text{.}$

    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\text{.}$ 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 $\int P\text{,}$ 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 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 $K\text{.}$ 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 $\mathrm{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\Rightarrow Y$ of presheaves expresses $Y$ as a cocone over $よ(\pi P)\text{.}$ 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 $\mathrm{id}$ is initial the coslice category under $P\text{.}$

    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\Rightarrow Y$ are two maps such that, for every map with representable domain $h:よ(A)\to X\text{,}$ $fh=gh\text{,}$ then $f=g\text{.}$ 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)\Rightarrow X$ can be seen as a “generalised element” of $X\text{,}$ 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 $よ(\pi X)\text{.}$

The construction Map→cocone-under lets us express $Y$ as a cocone under $よ(\pi X)$ in a way that $f$ becomes a cocone homomorphism $X\to Y\text{;}$ The condition that $g$ agrees with $f$ on all generalised elements with representable domains ensures that $g$ is also a cocone homomorphism $X\to Y\text{;}$ But $X$ is initial, so $f=g\text{!}$

  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\to Y$ in $\mathcal{C}$ extend to maps $よ(f),よ(g):よ(X)\to よ(Y)\text{,}$ and the functor $よ(-)$ is fully faithful, two maps in $\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 =
    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 _