open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Functor.Reasoning.Presheaf as PSh

open Functor
open _=>_

module Cat.Functor.Hom.Yoneda where


# The Yoneda lemmaπ

module _ {o β} {C : Precategory o β} (A : Functor (C ^op) (Sets β)) where
private module A = PSh A using (expand ; elim)
open Precategory C


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          β

module _ {o β} {C : Precategory o β} {A : Functor (C ^op) (Sets β)} where
private module A = PSh A
open Precategory C


## Naturalityπ

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

  yo-natr
: β {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

yo-naturalr
: β {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

  yo-natl
: β {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

yo-naturall
: β {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

  unyo-path : β {U : β C β} {x y : A Κ» U} β yo {C = C} A x β‘ yo A y β x β‘ y
unyo-path {x = x} {y} p =