module Cat.Functor.Hom.Yoneda where

The Yoneda lemmaπŸ”—

The Yoneda lemma says that the set of sections of a presheaf is isomorphic to the set of natural transformations into with domain a and that this isomorphism is natural. This result is actually extremely easy to prove, as long as we expand what a natural transformation consists of: a dependent function

There’s no secret in choosing the components of the isomorphism:

  • Given a we define a natural transformation by sending a map to the restriction
  yo : βˆ€ {U} β†’ A Κ» U β†’ Hom-into C U => A
  yo a .Ξ· i h = A βŸͺ h ⟫ a
  yo a .is-natural x y f = ext Ξ» h β†’ A.expand refl
  • Given an we obtain a value
  unyo : βˆ€ {U} β†’ Hom-into C U => A β†’ A Κ» U
  unyo h = h .Ξ· _ id

This inverse explains why the Yoneda lemma is sometimes stated as β€œnatural transformations (from a representable) are determined by their component at the identity”. These inverse equivalences compose to give expressions which are easy to cancel using naturality and functoriality:

  yo-is-equiv : βˆ€ {U} β†’ is-equiv (yo {U})
  yo-is-equiv = is-iso→is-equiv λ where
    .is-iso.inv  n β†’ unyo n
    .is-iso.rinv x β†’ ext Ξ» i h β†’
      yo (unyo x) .Ξ· i h β‰‘Λ˜βŸ¨ x .is-natural _ _ _ # _ βŸ©β‰‘Λ˜
      x .Ξ· i (id ∘ h)    β‰‘βŸ¨ ap (x .Ξ· i) (idl h) βŸ©β‰‘
      x .η i h           ∎
    .is-iso.linv x β†’
      A βŸͺ id ⟫ x β‰‘βŸ¨ A.elim refl βŸ©β‰‘
      x          ∎


The only part of the Yoneda lemma which is slightly tricky is working out the naturality statements. Since the isomorphism is natural in both and there are two statements. We implement the proofs of naturality for the isomorphism as combinators, so that they can slot into bigger proofs more easily. Calling these combinators with gives back the familiar naturality results.

For naturality β€œon the right”, i.e.Β in the coordinate, naturality says that given we have for all

    : βˆ€ {U V} {x : A Κ» U} {h : Hom V U} {y}
    β†’ A βŸͺ h ⟫ x ≑ y
    β†’ yo A x ∘nt γ‚ˆβ‚ C h ≑ yo A y
  yo-natr p = ext Ξ» i f β†’ A.expand refl βˆ™ A.ap p

    : βˆ€ {U V} {x : A Κ» U} {h : Hom V U}
    β†’ yo A x ∘nt γ‚ˆβ‚ C h ≑ yo A (A βŸͺ h ⟫ x)
  yo-naturalr = yo-natr refl

On β€œthe left”, i.e.Β in the variable naturality says that, given a natural transformation we have as natural transformations for any

    : βˆ€ {B : Functor (C ^op) (Sets β„“)} {U} {x : A Κ» U} {y : B Κ» U} {h : A => B}
    β†’ h .Ξ· U x ≑ y β†’ h ∘nt yo {C = C} A x ≑ yo B y
  yo-natl {B = B} {h = h} p = ext Ξ» i f β†’ h .is-natural _ _ _ # _ βˆ™ PSh.ap B p

    : βˆ€ {B : Functor (C ^op) (Sets β„“)} {U} {x : A Κ» U} {h : A => B}
    β†’ h ∘nt yo {C = C} A x ≑ yo B (h .Ξ· U x)
  yo-naturall = yo-natl refl