Yoneda Lemma

Yoneda.agda

module CatScratch where

open import Function hiding (_∘_; id)
open import Level
open import Data.Product
open import Relation.Binary
open import Relation.Binary.Core using (_≡_)
open import Relation.Binary.PropositionalEquality using (setoid)
import Relation.Binary.EqReasoning as EqR
import Relation.Binary.SetoidReasoning as SetR
open Setoid renaming (_≈_ to eqSetoid)

module Map where
  record Map {c₀ c₀′ ℓ ℓ′ : Level} (A : Setoid c₀ ℓ) (B : Setoid c₀′ ℓ′) : Set (suc (c₀ ⊔ ℓ ⊔ c₀′ ⊔ ℓ′)) where
    field
      mapping : Carrier A → Carrier B
      preserveEq : {x y : Carrier A} → (eqSetoid A x y) → eqSetoid B (mapping x) (mapping y)

  open Map public

  equality : {c₀ ℓ : Level} {A B : Setoid c₀ ℓ} (f g : Map A B) → Set _
  equality {A = A} {B = B} f g = ∀(x : Carrier A) → eqSetoid B (mapping f x) (mapping g x)

  compose : {c₀ ℓ : Level} {A B C : Setoid c₀ ℓ} (f : Map B C) (g : Map A B) → Map A C
  compose {C = C} f g = record {
    mapping = λ x → mapping f (mapping g x);
    preserveEq = λ x₁ → (preserveEq f (preserveEq g x₁)) }

  identity : {c₀ ℓ : Level} {A : Setoid c₀ ℓ} → Map A A
  identity = record { mapping = λ x → x ; preserveEq = λ x₁ → x₁ }

  subst : ∀{c₀ ℓ} {A B : Setoid c₀ ℓ} {f g : Map A B} (a : Carrier A) → equality f g → eqSetoid B (mapping f a) (mapping g a)
  subst a eq = eq a

module Category where
  record Category (C₀ C₁ ℓ : Level) : Set (suc (C₀ ⊔ C₁ ⊔ ℓ)) where
    field
      Obj : Set C₀
      Homsetoid : Obj → Obj → Setoid C₁ ℓ

    Hom : Obj → Obj → Set C₁
    Hom A B = Carrier (Homsetoid A B)

    equal : {A B : Obj} → Hom A B → Hom A B → Set ℓ
    equal {A} {B} f g = eqSetoid (Homsetoid A B) f g

    field
      comp : {A B C : Obj} → Hom B C → Hom A B → Hom A C
      id : {A : Obj} → Hom A A

    field
      leftId : {A B : Obj} {f : Hom A B} → equal (comp id f) f
      rightId : {A B : Obj} {f : Hom A B} → equal (comp f id) f
      assoc : {A B C D : Obj} {f : Hom A B} {g : Hom B C} {h : Hom C D}
        → equal (comp (comp h g) f) (comp h (comp g f))
      ≈-composite : {A B C : Obj} {f g : Hom B C} {h i : Hom A B}
        → equal f g → equal h i → equal (comp f h) (comp g i)

    dom : {A B : Obj} → Hom A B → Obj
    dom {A} _ = A

    cod : {A B : Obj} → Hom A B → Obj
    cod {B} _ = B

    op : Category C₀ C₁ ℓ
    op = record
      { Obj = Obj
      ; Homsetoid = flip Homsetoid
      ; comp = flip comp
      ; id = id

      ; leftId = rightId
      ; rightId = leftId
      ; assoc = λ{A B C D} → IsEquivalence.sym (isEquivalence (Homsetoid D A)) assoc
      ; ≈-composite = flip ≈-composite
      }

  open Category public

  infixr 9 _∘_
  infixr 7 _[_∘_]
  infixr 2 _≈_
  infixr 2 _[_≈_]
  infix 4 _[_≅_]

  _[_∘_] : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
  C [ f ∘ g ] = comp C f g

  _∘_ : ∀{C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
  _∘_ {C = C} = _[_∘_] C

  _[_≈_] : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} → Rel (Hom C A B) ℓ
  C [ f ≈ g ] = equal C f g

  _≈_ : ∀{C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {A B : Obj C} → Rel (Hom C A B) ℓ
  _≈_ {C = C} = equal C

  equiv : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} → IsEquivalence (eqSetoid (Homsetoid C A B))
  equiv C {A} {B} = isEquivalence (Homsetoid C A B)

  refl-hom : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} {f : Hom C A B} → C [ f ≈ f ]
  refl-hom C = IsEquivalence.refl (equiv C)

  sym-hom : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → C [ g ≈ f ]
  sym-hom C = IsEquivalence.sym (equiv C)

  trans-hom : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} {f g h : Hom C A B} → C [ f ≈ g ] → C [ g ≈ h ] → C [ f ≈ h ]
  trans-hom C = IsEquivalence.trans (equiv C)

  record _[_≅_] {C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) (a b : Obj C) : Set (C₀ ⊔ C₁ ⊔ ℓ) where
    field
      map-→ : Hom C a b
      map-← : Hom C b a
      iso : (C [ C [ map-→ ∘ map-← ] ≈ id C ]) × (C [ C [ map-← ∘ map-→ ] ≈ id C ])

open Category

Setoids : {c₀ ℓ : Level} → Category (suc (c₀ ⊔ ℓ)) (suc (c₀ ⊔ ℓ)) (c₀ ⊔ ℓ)
Setoids {c₀} {ℓ} = record {
  Obj = Setoid c₀ ℓ;
  Homsetoid = λ A B → record { Carrier = Map.Map A B; _≈_ = Map.equality; isEquivalence = Map-Equal-Equiv A B };
  comp = Map.compose;
  id = Map.identity;
  leftId = λ {_ B} _ → refl B;
  rightId = λ {_ B} _ → refl B;
  assoc = λ {_ _ _ D} x → refl D;
  ≈-composite = λ {_ _ C f g h} x x₁ x₂ → trans C (x (Map.Map.mapping h x₂)) (Map.Map.preserveEq g (x₁ x₂)) }
  where
    Map-Equal-Equiv : (A B : Setoid _ _) → IsEquivalence Map.equality
    Map-Equal-Equiv A B = record { refl = λ _ → refl B ; sym = λ x x₁ → sym B (x x₁) ; trans = λ x x₁ x₂ → trans B (x x₂) (x₁ x₂) }

module CategoryReasoning where
  infix 1 begin⟨_⟩_
  infixr 2 _≈⟨_⟩_ _≡⟨_⟩_
  infix 3 _∎

  data IsRelatedTo[_] {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) (a b : Obj C) (x y : Hom C a b) : Set ℓ where
    relTo : C [ x ≈ y ] → IsRelatedTo[ C ] a b x y

  begin⟨_⟩_ : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) → {A B : Obj C} {f g : Hom C A B} → IsRelatedTo[ C ] A B f g → equal C f g
  begin⟨_⟩_ C {A} {B} (relTo x≈y) = x≈y

  _∎ : ∀ {c₀ c₁ ℓ} {C : Category c₀ c₁ ℓ} {A B : Obj C} (f : Hom C A B) → IsRelatedTo[ C ] A B f f
  _∎ {C = C} f = relTo (refl-hom C)

  _≈⟨_⟩_ : ∀ {c₀ c₁ ℓ} {C : Category c₀ c₁ ℓ} → {A B : Obj C} (f : Hom C A B) → {g h : Hom C A B} → equal C f g → IsRelatedTo[ C ] A B g h → IsRelatedTo[ C ] A B f h
  _≈⟨_⟩_ {C = C} f f≈g (relTo g≈h) = relTo (trans-hom C f≈g g≈h)

  _≡⟨_⟩_ : ∀ {c₀ c₁ ℓ} {C : Category c₀ c₁ ℓ} → {A B : Obj C} (f : Hom C A B) → {g h : Hom C A B} → f ≡ g → IsRelatedTo[ C ] A B g h → IsRelatedTo[ C ] A B f h
  _≡⟨_⟩_ {C = C} f _≡_.refl (relTo g≈h) = relTo g≈h

open CategoryReasoning

module Functor where
  record Functor {c₀ c₁ ℓ c₀′ c₁′ ℓ′} (C : Category c₀ c₁ ℓ) (D : Category c₀′ c₁′ ℓ′) : Set (suc (c₀ ⊔ c₀′ ⊔ c₁ ⊔ c₁′ ⊔ ℓ ⊔ ℓ′)) where
    field
      fobj : Obj C → Obj D
      fmapsetoid : {A B : Obj C} → Map.Map (Homsetoid C A B) (Homsetoid D (fobj A) (fobj B))

    fmap : {A B : Obj C} → Hom C A B → Hom D (fobj A) (fobj B)
    fmap {A} {B} = Map.Map.mapping (fmapsetoid {A} {B})

    field
      preserveId : {A : Obj C} → D [ fmap (id C {A}) ≈ id D {fobj A} ]
      preserveComp : {a b c : Obj C} (f : Hom C b c) (g : Hom C a b) → D [ fmap (C [ f ∘ g ]) ≈ (D [ fmap f ∘ fmap g ]) ]

  open Functor

  preserveEq : ∀ {c₀ c₁ ℓ c₀′ c₁′ ℓ′} {C : Category c₀ c₁ ℓ} {D : Category c₀′ c₁′ ℓ′} {A B : Obj C} {x y : Category.Hom C A B} (F : Functor C D) → C [ x ≈ y ] → D [ fmap F x ≈ fmap F y ]
  preserveEq F xy = Map.Map.preserveEq (fmapsetoid F) xy

  compose : ∀ {c₀ c₁ ℓ c₀′ c₁′ ℓ′ c₀″ c₁″ ℓ″} {C : Category c₀ c₁ ℓ} {D : Category c₀′ c₁′ ℓ′} {E : Category c₀″ c₁″ ℓ″} → Functor {c₀′} {c₁′} {ℓ′} {c₀″} {c₁″} {ℓ″} D E → Functor {c₀} {c₁} {ℓ} {c₀′} {c₁′} {ℓ′} C D → Functor {c₀} {c₁} {ℓ} {c₀″} {c₁″} {ℓ″} C E
  compose {C = C} {D} {E} G F = record {
    fobj = λ x → fobj G (fobj F x);
    fmapsetoid = record { mapping = λ f → fmap G (fmap F f) ; preserveEq = λ {x} {y} x≈y → begin⟨ E ⟩
      fmap G (fmap F x) ≈⟨ preserveEq G (begin⟨ D ⟩
        fmap F x ≈⟨ preserveEq F x≈y ⟩
        fmap F y ∎) ⟩
      fmap G (fmap F y) ∎
    };
    preserveId = begin⟨ E ⟩
      fmap G (fmap F (id C)) ≈⟨ preserveEq G (preserveId F) ⟩
      fmap G (id D) ≈⟨ preserveId G ⟩
      (id E) ∎;
    preserveComp = λ f g → begin⟨ E ⟩
      fmap G (fmap F (C [ f ∘ g ])) ≈⟨ preserveEq G (preserveComp F f g) ⟩
      fmap G (D [ fmap F f ∘ fmap F g ]) ≈⟨ preserveComp G (fmap F f) (fmap F g) ⟩
      (E [ fmap G (fmap F f) ∘ fmap G (fmap F g) ]) ∎
    }

  identity : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) → Functor {c₀} {c₁} {ℓ} {c₀} {c₁} {ℓ} C C
  identity C = record {
    fobj = λ x → x ;
    fmapsetoid = record { mapping = λ x → x ; preserveEq = λ x₁ → x₁ } ;
    preserveId = refl-hom C ; preserveComp = λ _ _ → refl-hom C }

  data _[_~_]
    {C₀ C₁ ℓ : Level} (C : Category C₀ C₁ ℓ) {A B : Obj C} (f : Hom C A B)
    : ∀{X Y : Obj C} → Hom C X Y → Set (suc (C₀ ⊔ C₁ ⊔ ℓ)) where
    eqArrow : {g : Hom C A B} → C [ f ≈ g ] → C [ f ~ g ]

  eqArrowRefl : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {A B : Obj C} {f : Hom C A B} → C [ f ~ f ]
  eqArrowRefl C = eqArrow (refl-hom C)

  eqArrowSym : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {X Y Z W : Obj C} {f : Hom C X Y} {g : Hom C Z W} → C [ f ~ g ] → C [ g ~ f ]
  eqArrowSym C (eqArrow f~g) = eqArrow (sym-hom C f~g)

  eqArrowTrans : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {X Y Z W S T : Obj C} {f : Hom C X Y} {g : Hom C Z W} {h : Hom C S T} → C [ f ~ g ] → C [ g ~ h ] → C [ f ~ h ]
  eqArrowTrans C (eqArrow f~g) (eqArrow g~h) = eqArrow (trans-hom C f~g g~h)

  eqArrowFmap : ∀ {c₀ c₁ ℓ c₀′ c₁′ ℓ′} {C : Category c₀ c₁ ℓ} {D : Category c₀′ c₁′ ℓ′} {X Y Z W : Obj C} {x : Category.Hom C X Y} {y : Category.Hom C Z W} (F : Functor C D) → C [ x ~ y ] → D [ fmap F x ~ fmap F y ]
  eqArrowFmap F (eqArrow x~y) = eqArrow (preserveEq F x~y)

  equality : ∀ {c₀ c₁ ℓ} {C D : Category c₀ c₁ ℓ} → (F G : Functor C D) → _
  equality {C = C} {D} F G = ∀ {A B : Obj C} (f : Hom C A B) → D [ fmap F f ~ fmap G f ]

open Functor.Functor

Cat : ∀ {c₀ c₁ ℓ} → Category (suc (c₀ ⊔ c₁ ⊔ ℓ)) _ _
Cat {c₀} {c₁} {ℓ} = record {
  Obj = Category c₀ c₁ ℓ;
  Homsetoid = λ A B → record {
    Carrier = Functor.Functor A B ; _≈_ = Functor.equality ;
    isEquivalence = record {
      refl = λ f → Functor.eqArrowRefl B ;
      sym = λ x f → Functor.eqArrowSym B (x f);
      trans = λ x x₁ f → Functor.eqArrowTrans B (x f) (x₁ f) } };
  comp = Functor.compose;
  id = λ {A} → Functor.identity A;
  leftId = λ {A} {B} {f} f₁ → Functor.eqArrow (refl-hom B);
  rightId = λ {A} {B} {f} f₁ → Functor.eqArrow (refl-hom B);
  assoc = λ {A} {B} {C} {D} {f} {g} {h} f₁ → Functor.eqArrow (begin⟨ D ⟩
    fmap (Functor.compose (Functor.compose h g) f) f₁ ≈⟨ refl-hom D ⟩
    fmap h (fmap g (fmap f f₁)) ≈⟨ refl-hom D ⟩
    fmap (Functor.compose h (Functor.compose g f)) f₁
    ∎);
  ≈-composite = λ {A} {B} {C} {f} {g} {h} {i} f~g h~i f₁ → Functor.eqArrowTrans C (f~g (fmap h f₁)) (Functor.eqArrowFmap g (h~i f₁))
  }

module Nat where
  record Nat {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} (F G : Functor.Functor C D) : Set (suc (C₀ ⊔ C₁ ⊔ ℓ ⊔ D₀ ⊔ D₁ ⊔ ℓ′)) where
    field
      component : (X : Obj C) → Hom D (fobj F X) (fobj G X)

    field
      naturality : {a b : Obj C} {f : Hom C a b}
        → D [ D [ component b ∘ fmap F f ] ≈ D [ fmap G f ∘ component a ] ]

  open Nat

  identity : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} → (F : Functor.Functor C D) → Nat F F
  identity {D = D} F = record {
    component = λ X → id D ;
    naturality = λ {a} {b} {f} → trans-hom D (leftId D) (sym-hom D (rightId D)) }

  compose : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} → {F G H : Functor.Functor C D} → Nat G H → Nat F G → Nat F H
  compose {C = C} {D} {F} {G} {H} η ε  = record {
    component = λ X → D [ component η X ∘ component ε X ] ;
    naturality = λ {a} {b} {f} → (begin⟨ D ⟩
      D [ (D [ component η b ∘ component ε b ]) ∘ fmap F f ] ≈⟨ assoc D ⟩
      D [ component η b ∘ (D [ component ε b ∘ fmap F f ]) ] ≈⟨ ≈-composite D (refl-hom D) (naturality ε) ⟩
      D [ component η b ∘ (D [ fmap G f ∘ component ε a ]) ] ≈⟨ sym-hom D (assoc D) ⟩
      D [ (D [ component η b ∘ fmap G f ]) ∘ component ε a ] ≈⟨ ≈-composite D (naturality η) (refl-hom D) ⟩
      D [ (D [ fmap H f ∘ component η a ]) ∘ component ε a ] ≈⟨ assoc D ⟩
      D [ fmap H f ∘ (D [ component η a ∘ component ε a ]) ] ∎) }

  equality : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F G : Functor.Functor C D} → (η τ : Nat F G) → Set _
  equality {C = C} {D} η τ = ∀ {a : Obj C} → D [ component η a ≈ component τ a ]

  subst : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F G : Functor.Functor C D} {η τ : Nat F G} → (a : Obj C) → equality η τ → D [ component η a ≈ component τ a ]
  subst a eq = eq {a}

open Nat.Nat

Hom[_][_,-] : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) (X : Obj C) → Functor.Functor C Setoids
Hom[_][_,-] C X = record {
  fobj = λ x → (Homsetoid C X x) ;
  fmapsetoid = record {
    mapping = λ x → record { mapping = λ x₁ → C [ x ∘ x₁ ] ; preserveEq = ≈-composite C (refl-hom C) } ;
    preserveEq = λ x₁ x₂ → ≈-composite C x₁ (refl-hom C) } ;
  preserveId = λ x → leftId C ;
  preserveComp = λ f g x → assoc C }

HomNat[_][_,-] : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {A B : Obj C} (f : Hom C A B) → Nat.Nat (Hom[ C ][ B ,-]) (Hom[ C ][ A ,-])
HomNat[_][_,-] C {A} {B} f = record {
  component = component-map ;
  naturality = λ {a} {b} {x} → λ x₁ → begin⟨ C ⟩
    Map.mapping (Setoids [ component-map b ∘ fmap Hom[ C ][ B ,-] x ]) x₁ ≈⟨ refl-hom C ⟩
    C [ C [ x ∘ x₁ ] ∘ f ] ≈⟨ assoc C ⟩
    C [ x ∘ C [ x₁ ∘ f ] ] ≈⟨ refl-hom C ⟩
    Map.mapping (Setoids [ fmap Hom[ C ][ A ,-] x ∘ component-map a ]) x₁
  ∎ }
  where
    component-map = λ X → record {
      mapping = λ x → C [ x ∘ f ] ;
      preserveEq = λ x₁ → ≈-composite C x₁ (refl-hom C) }

Hom[_][-,_] : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) (X : Obj C) → Functor.Functor (op C) Setoids
Hom[_][-,_] C X = record {
  fobj = λ x → (Homsetoid C x X) ;
  fmapsetoid = record {
    mapping = λ x → record { mapping = λ x₁ → C [ x₁ ∘ x ] ; preserveEq = ≈-composite (op C) (refl-hom C) } ;
    preserveEq = λ x₁ x₂ → ≈-composite (op C) x₁ (refl-hom C) } ;
  preserveId = λ x → leftId (op C) ;
  preserveComp = λ f g x → assoc (op C) }

HomNat[_][-,_] : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {A B : Obj C} (f : Hom C A B) → Nat.Nat (Hom[ C ][-, A ]) (Hom[ C ][-, B ])
HomNat[_][-,_] C {A} {B} f = record {
  component = component-map ;
  naturality = λ {a} {b} {x} → λ x₁ → begin⟨ C ⟩
    Map.mapping (Setoids [ component-map b ∘ fmap Hom[ C ][-, A ] x ]) x₁ ≈⟨ refl-hom C ⟩
    C [ f ∘ C [ x₁ ∘ x ] ] ≈⟨ sym-hom C (assoc C) ⟩
    C [ C [ f ∘ x₁ ] ∘ x ] ≈⟨ refl-hom C ⟩
    Map.mapping (Setoids [ fmap Hom[ C ][-, B ] x ∘ component-map a ]) x₁
  ∎ }
  where
    component-map = λ X → record {
      mapping = λ x → C [ f ∘ x ] ;
      preserveEq = λ x₁ → ≈-composite C (refl-hom C) x₁ }

FunCat : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} → (Category C₀ C₁ ℓ) → (Category D₀ D₁ ℓ′) → Category _ _ _
FunCat C D = record {
  Obj = Functor.Functor C D;
  Homsetoid = λ F G → record { Carrier = Nat.Nat F G ; _≈_ = Nat.equality ; isEquivalence = record {
    refl = λ {x} {a} → refl-hom D ;
    sym = λ x → λ {a} → sym-hom D x ;
    trans = λ x x₁ → λ {a} → trans-hom D x x₁ } };
  comp = Nat.compose;
  id = λ {A} → Nat.identity A;
  leftId = λ {A} {B} {f} {a} → leftId D;
  rightId = λ {A} {B} {f} {a} → rightId D;
  assoc = λ {A} {B} {C₁} {D₁} {f} {g} {h} {a} → assoc D;
  ≈-composite = λ x x₁ → ≈-composite D x x₁
  }

[_,_] : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} (C : Category C₀ C₁ ℓ) → (D : Category D₀ D₁ ℓ′) → Category _ _ _
[ C , D ] = FunCat C D

PSh[_] : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) → Category _ _ _
PSh[_] {_} {C₁} {ℓ} C = [ op C , Setoids {C₁} {ℓ} ]

yoneda : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) → Functor.Functor C (PSh[ C ])
yoneda C = record {
  fobj = λ x → Hom[ C ][-, x ] ;
  fmapsetoid = λ {A} {B} → record { mapping = λ f → HomNat[ C ][-, f ] ; preserveEq = λ {x} {y} x₁ x₂ → begin⟨ C ⟩
    Map.mapping (component HomNat[ C ][-, x ] _) x₂ ≈⟨ refl-hom C ⟩
    C [ x ∘ x₂ ] ≈⟨ ≈-composite C x₁ (refl-hom C) ⟩
    C [ y ∘ x₂ ] ≈⟨ refl-hom C ⟩
    Map.mapping (component HomNat[ C ][-, y ] _) x₂
  ∎ } ;
  preserveId = λ x → leftId C ;
  preserveComp = λ f g x → assoc C
  }

LiftSetoid : ∀ {a b ℓ ℓ′} (A : Setoid a ℓ) → Setoid (a ⊔ b) (ℓ ⊔ ℓ′)
LiftSetoid {a} {b} {ℓ} {ℓ′} A = record {
  Carrier = Lift {a} {b} (Carrier A) ;
  _≈_ = λ x x₁ → Lift {ℓ} {ℓ′} (eqSetoid A (lower x) (lower x₁)) ;
  isEquivalence = record {
    refl = lift (refl A) ;
    sym = λ x → lift (sym A (lower x)) ;
    trans = λ x x₁ → lift (trans A (lower x) (lower x₁)) } }

YonedaLemma : ∀{C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {F : Obj PSh[ C ]} {X : Obj C} → Setoids [ Homsetoid [ op C , Setoids ] (fobj (yoneda C) X) F ≅ LiftSetoid {C₁} {suc (suc ℓ) ⊔ (suc (suc C₁) ⊔ suc C₀)} {ℓ} {C₀ ⊔ C₁ ⊔ ℓ} (fobj F X) ]
YonedaLemma {C₀} {C₁} {ℓ} {C} {F} {X} = record {
  map-→ = nat→obj ;
  map-← = obj→nat ;
  iso = obj→obj≈id , nat→nat≈id }
  where
    nat→obj : Map.Map (Homsetoid [ op C , Setoids ] (fobj (yoneda C) X) F) (LiftSetoid (fobj F X))
    nat→obj = record {
      mapping = λ α → lift (Map.mapping (component α X) (id C)) ;
      preserveEq = λ x≈y → lift (x≈y (id C)) }

    obj→nat : Map.Map (LiftSetoid (fobj F X)) (Homsetoid [ op C , Setoids ] (fobj (yoneda C) X) F)
    obj→nat = record {
      mapping = λ a → record {
        component = component-map a ;
        naturality = λ {c} {d} {f} x → SetR.begin⟨ fobj F d ⟩
          Map.mapping (Setoids [ component-map a d ∘ fmap (fobj (yoneda C) X) f ]) x SetR.≈⟨ refl (fobj F d) ⟩
          Map.mapping (Map.mapping (fmapsetoid F) (C [ x ∘ f ])) (lower a) SetR.≈⟨ (preserveComp F f x) (lower a) ⟩
          Map.mapping (Map.mapping (fmapsetoid F) f) (Map.mapping (Map.mapping (fmapsetoid F) x) (lower a)) SetR.≈⟨ refl (fobj F d) ⟩
          Map.mapping (Setoids [ fmap F f ∘ component-map a c ]) x
        SetR.∎} ;
      preserveEq = λ {x} {y} x≈y f → SetR.begin⟨ fobj F _ ⟩
        Map.mapping (component-map x _) f SetR.≈⟨ refl (fobj F _) ⟩
        Map.mapping (Map.mapping (fmapsetoid F) f) (lower x) SetR.≈⟨ Map.preserveEq (fmap F f) (lower x≈y) ⟩
        Map.mapping (Map.mapping (fmapsetoid F) f) (lower y) SetR.≈⟨ refl (fobj F _) ⟩
        Map.mapping (component-map y _) f
        SetR.∎}
      where
        component-map = λ a b → record {
          mapping = λ u → Map.mapping (fmap F u) (lower a) ;
          preserveEq = λ {x} {y} x≈y → SetR.begin⟨ fobj F b ⟩
            Map.mapping (fmap F x) (lower a) SetR.≈⟨ (Functor.preserveEq F x≈y) (lower a) ⟩
            Map.mapping (fmap F y) (lower a)
          SetR.∎
          }

    obj→obj≈id : Setoids [ Setoids [ nat→obj ∘ obj→nat ] ≈ id Setoids ]
    obj→obj≈id = λ x → lift (SetR.begin⟨ fobj F X ⟩
      lower (Map.mapping (Setoids [ nat→obj ∘ obj→nat ]) x) SetR.≈⟨ refl (fobj F X) ⟩
      Map.mapping (Map.mapping (fmapsetoid F) (id C)) (lower x) SetR.≈⟨ (preserveId F) (lower x) ⟩
      lower x SetR.≈⟨ refl (fobj F X) ⟩
      lower (Map.mapping {A = LiftSetoid {ℓ′ = ℓ} (fobj F X)} (id Setoids) x)
      SetR.∎)

    nat→nat≈id : Setoids [ Setoids [ obj→nat ∘ nat→obj ] ≈ id Setoids ]
    nat→nat≈id α f = SetR.begin⟨ fobj F _ ⟩
      Map.mapping (component (Map.mapping (Setoids [ obj→nat ∘ nat→obj ]) α) _) f SetR.≈⟨ refl (fobj F _) ⟩
      Map.mapping (Setoids [ fmap F f ∘ component α X ]) (id C) SetR.≈⟨ lemma (id C) ⟩
      Map.mapping (Setoids [ component α (dom C f) ∘ fmap (fobj (yoneda C) X) f ]) (id C) SetR.≈⟨ Map.preserveEq (component α (dom C f)) (leftId C) ⟩
      Map.mapping (component α (dom C f)) f SetR.≈⟨ refl (fobj F _) ⟩
      Map.mapping (component (Map.mapping (id Setoids {Homsetoid [ (op C) , Setoids ] _ _}) α) (dom C f)) f
      SetR.∎
      where
        lemma : Setoids [ Setoids [ fmap F f ∘ component α X ] ≈ Setoids [ component α (dom C f) ∘ fmap (fobj (yoneda C) X) f ] ]
        lemma = sym-hom Setoids {f = Setoids [ component α (dom C f) ∘ fmap (fobj (yoneda C) X) f ]} {g = Setoids [ fmap F f ∘ component α X ]} (naturality α)