🔍

Equations Inline Footnotes

open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Instances.Sets
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Functor.Reasoning.Presheaf as PSh

open _=>_ hiding (op)
open Functor

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 $A(U)$ of a presheaf $A$ is isomorphic to the set $\mathcal{C}(-,U)\Rightarrow A$ of natural transformations into $A\text{,}$ with domain a $\mathbf{Hom}\text{-functor;}$ and that this isomorphism is natural. This result is actually extremely easy to prove, as long as we expand what a natural transformation $\eta :\mathcal{C}(-,U)\Rightarrow A$ consists of: a dependent function $$\eta :\prod _{V:\mathcal{C}}\mathcal{C}(V,U)\to A(V)\text{.}$$

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

• Given a $x:A(U)\text{,}$ we define a natural transformation $\mathrm{yo}x$ by sending a map $h:\mathcal{C}(V,U)$ to the restriction $A(h)(x):A(V)\text{.}$

  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 $\eta :\mathcal{C}(-,U)\Rightarrow A\text{,}$ we obtain a value ${\eta }_U(\mathrm{id}):A(U)\text{.}$

  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.from   → unyo
    .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 $$(\mathcal{C}(-,U)\Rightarrow A)\simeq A(U)$$ is natural in both $A$ and $U\text{,}$ there are two statements. We implement the proofs of naturality for the $\mathrm{yo}\text{-}$ $\mathrm{unyo}$ isomorphism as combinators, so that they can slot into bigger proofs more easily. Calling these combinators with $\mathrm{refl}$ gives back the familiar naturality results.

For naturality “on the right”, i.e. in the $U$ coordinate, naturality says that given $h:V\to U\text{,}$ we have for all $x\text{,}$ $$\mathrm{yo}(x)\circ \mathcal{C}(-,h)=\mathrm{yo}(A(h)(x))\text{.}$$

  yo-natr : ∀ {U V x y} {h : Hom V U} → A ⟪ h ⟫ x ≡ y → yo A x ∘nt よ C .F₁ h ≡ yo A y
  yo-natr p = ext λ i f → A.expand refl ∙ A.ap p

  yo-naturalr : ∀ {U V x} {h : Hom V U} → yo A x ∘nt よ C .F₁ h ≡ yo A (A ⟪ h ⟫ x)
  yo-naturalr = yo-natr refl

On “the left”, i.e. in the variable $A\text{,}$ naturality says that, given a natural transformation $\eta :A\Rightarrow B\text{,}$ we have $$\eta \circ {\mathrm{yo}}_A(x)={\mathrm{yo}}_B({\eta }_U(x))\text{,}$$ as natural transformations $\mathcal{C}(-,U)\Rightarrow B\text{,}$ for any $x:A(U)\text{.}$

  yo-natl : ∀ {B U x y h} → h .η U x ≡ y → h ∘nt yo 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 U x h} → h ∘nt yo A x ≡ yo B (h .η U x)
  yo-naturall = yo-natl refl

  unyo-path : ∀ {U} {x y : A ʻ U} → yo A x ≡ yo A y → x ≡ y
  unyo-path {x = x} {y} p =
    x          ≡⟨ A.intro refl ⟩≡
    A ⟪ id ⟫ x ≡⟨ unext p _ id ⟩≡
    A ⟪ id ⟫ y ≡⟨ A.elim refl ⟩≡
    y          ∎

Finally, we can package the lemma into the statement that there is a natural isomorphism between bifunctors ${\mathcal{C}}^{\mathrm{op}}\times [{\mathcal{C}}^{\mathrm{op}},\mathbf{Sets}]\to \mathbf{Sets}\text{,}$ where on the one hand we have the bifunctor which acts on an object $U:\mathcal{C}$ and a presheaf $A:{\mathcal{C}}^{\mathrm{op}}\to \mathbf{Sets}$ by evaluating $A$ at $U\text{,}$ and on the other hand, the bifunctor which computes the set of natural transformations from $\mathcal{C}(-,U)$ to $A\text{.}$

module _ {κ} {C : Precategory κ κ} where
  open Precategory C

  yoneda : Flip Id ≅ⁿ よcov (PSh κ C) F∘ op (よ C)
  yoneda = biiso→isoⁿ
    (λ _ A → equiv→iso (yo A , yo-is-equiv A))
    (λ _ → funext λ _ → yo-naturalr)
    (λ _ → funext λ _ → yo-naturall)