Yoneda Lemma Proof under Higher-Order types

YonedaHO.agda

module YonedaHO where

open import Agda.Primitive using (Level; lsuc; _⊔_)
open import Level using (lift)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; cong-app)
open import Data.Product using (_×_; ∃; _,_; proj₂)

{- apply _≡_ for objects and morphisms for Locally Small Categories -}

{- morphism type definition -}
Hom : (o m : Level) → Set (lsuc o ⊔ lsuc m)
Hom o m = Set o → Set o → Set m

{- Category definition -}
record Cat
  {o m}
  (hom : Hom o m)
  : Set (lsuc o ⊔ lsuc m) where

  infix 5 _⟿_
  _⟿_ = hom

  infixr 9 compose
  syntax compose f g = f ∘ g

  field
    id : ∀{a} → a ⟿ a
    compose : ∀ {a b c} → (b ⟿ c) → (a ⟿ b) → (a ⟿ c)
    left-id : ∀ {a b} (f : a ⟿ b) → id ∘ f ≡ f
    right-id : ∀ {a b} (f : a ⟿ b) → f ∘ id ≡ f
    associativity : ∀ {a b c d} (f : c ⟿ d) (g : b ⟿ c) (h : a ⟿ b) →
                    (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)

get-homᵒᵖ : ∀{o m} → Hom o m → Hom o m
get-homᵒᵖ hom a b = hom b a

_ᵒᵖ : ∀ {o m} {hom : Hom o m} → Cat hom → Cat (get-homᵒᵖ hom)
_ᵒᵖ {o} {m} {hom} C =
  record
  { id = idᵒᵖ
  ; compose = _∘ᵒᵖ_
  ; left-id = left-idᵒᵖ
  ; right-id = right-idᵒᵖ
  ; associativity = associativityᵒᵖ
  }
  where
    _⟿_ = hom
    _⟿ᵒᵖ_ = get-homᵒᵖ (_⟿_)
    infix 5 _⟿_ _⟿ᵒᵖ_

    idᵒᵖ = Cat.id C

    _∘_ : ∀ {a b c} → (b ⟿ c) → (a ⟿ b) → (a ⟿ c)
    _∘_ = Cat.compose C
    _∘ᵒᵖ_ : ∀ {a b c} → (b ⟿ᵒᵖ c) → (a ⟿ᵒᵖ b) → (a ⟿ᵒᵖ c)
    f ∘ᵒᵖ g = g ∘ f
    infixr 9  _∘_ _∘ᵒᵖ_

    left-idᵒᵖ : ∀ {a b} (f : a ⟿ᵒᵖ b) → idᵒᵖ ∘ᵒᵖ f ≡ f
    left-idᵒᵖ = Cat.right-id C

    right-idᵒᵖ : ∀ {a b} (f : a ⟿ᵒᵖ b) → f ∘ᵒᵖ idᵒᵖ ≡ f
    right-idᵒᵖ = Cat.left-id C

    associativityᵒᵖ : ∀ {a b c d} (f : c ⟿ᵒᵖ d) (g : b ⟿ᵒᵖ c) (h : a ⟿ᵒᵖ b) →
                      (f ∘ᵒᵖ g) ∘ᵒᵖ h ≡ f ∘ᵒᵖ (g ∘ᵒᵖ h)
    associativityᵒᵖ f g h = sym (Cat.associativity C h g f)

infix 9 _ᵒᵖ

{- Functor definition -}
record Functor
  {o₁ m₁}
  {hom₁ : Hom o₁ m₁}
  (C₁ : Cat hom₁)
  {o₂ m₂}
  {hom₂ : Hom o₂ m₂}
  (C₂ : Cat hom₂)
  : Set (lsuc o₁ ⊔ lsuc m₁ ⊔ lsuc o₂ ⊔ lsuc m₂) where

  _⟿₁_ = hom₁
  infix 5 _⟿₁_

  id₁ = Cat.id C₁
  _∘₁_ = Cat.compose C₁

  _⟿₂_ = hom₂

  id₂ = Cat.id C₂
  _∘₂_ = Cat.compose C₂

  infixr 9  _∘₁_ _∘₂_

  field
    F : Set o₁ → Set o₂
    fmap : ∀ {a b} → (a ⟿₁ b) → (F a ⟿₂ F b)
    fmap-id : ∀ {a} → fmap {a} {a} id₁ ≡ id₂
    fmap-dist : ∀ {a b c} {f : b ⟿₁ c} {g : a ⟿₁ b} →
                fmap {a} {c} (f ∘₁ g) ≡ fmap {b} {c} f ∘₂ fmap {a} {b} g

{- Naturality type -}
Naturality : ∀ {o m}   {hom  : Hom o m}    {C : Cat hom}
                {oᴰ mᴰ} {homᴰ : Hom oᴰ mᴰ} {D : Cat homᴰ} →
                Functor C D                                    →
                Functor C D                                    →
                Set (lsuc o ⊔ m ⊔ mᴰ)
Naturality
  {o}  {m}  {hom}  {C}
  {oᴰ} {mᴰ} {homᴰ} {D}
  rF
  rG
  = (Nat : ∀ a → F a ⟿ᴰ G a) →
    (∀ {a b} (f : a ⟿ b) → Nat b ∘ᴰ fmapF {a} {b} f ≡ fmapG {a} {b} f ∘ᴰ Nat a)
  where
    _⟿_  = hom
    _⟿ᴰ_ = homᴰ

    infix 5 _⟿_ _⟿ᴰ_

    _∘ᴰ_ = Cat.compose D
    infixr 9  _∘ᴰ_

    F = Functor.F rF
    fmapF = Functor.fmap rF

    G = Functor.F rG
    fmapG = Functor.fmap rG

---

{- extensionality type -}
EX : ∀ (lᵢ lⱼ : Level) -> Set (lsuc lᵢ ⊔ lsuc lⱼ)
EX lᵢ lⱼ =
  {A : Set lᵢ} {B : A → Set lⱼ} {f g : (x : A) → B x} →
  (∀ x → f x ≡ g x) → f ≡ g

{- hom-set of universe polymorphic Sets -}
_→ᵤ_ : ∀{l} -> Set l → Set l → Set l
_→ᵤ_ a b = a → b

{- universe polymorphic Sets definition -}
𝕊𝕖𝕥 : ∀ {l : Level} → Cat (_→ᵤ_ {l})
𝕊𝕖𝕥 =
  record
  { id = λ {a} (x : a) → x
  ; compose = λ f g x → f (g x)
  ; left-id  = λ f → refl
  ; right-id = λ f → refl
  ; associativity = λ f g h → refl
  }

module WithSets
  {l : Level}
  (extensionality : ∀{lᵢ lⱼ} → EX lᵢ lⱼ)
  where
    _→₀_ : Set l → Set l → Set l
    _→₀_ = _→ᵤ_ {l}
    𝕊𝕖𝕥₀ : Cat (_→₀_)
    𝕊𝕖𝕥₀ = 𝕊𝕖𝕥

    idₛ : ∀ {a : Set l} → a →₀ a
    idₛ = Cat.id 𝕊𝕖𝕥₀
    _∘ₛ_ = Cat.compose 𝕊𝕖𝕥₀
    infixr 9  _∘ₛ_

    homF : ∀ {o} {hom : Hom o l} (C : Cat hom) (r : Set o) → Functor C 𝕊𝕖𝕥₀
    homF {o} {hom} C r =
      record
      { F = Homᵣ
      ; fmap = fmapʰ
      ; fmap-id = fmapʰ-id
      ; fmap-dist = fmapʰ-dist
      }
      where
        {- hom-set of C -}
        _⟿_ = hom
        infix 5 _⟿_

        id : ∀ {a : Set o} → (a ⟿ a)
        id = Cat.id C
        _∘_ = Cat.compose C
        infixr 9  _∘_

        Homᵣ : Set o → Set l
        Homᵣ = _⟿_ r

        fmapʰ : ∀ {a b : Set o} → (a ⟿ b) → (r ⟿ a) → (r ⟿ b)
        fmapʰ = Cat.compose C

        fmapʰ-id : ∀ {a : Set o} → fmapʰ {a} {a} id ≡ idₛ
        fmapʰ-id = extensionality (Cat.left-id C)

        fmapʰ-dist : ∀ {a b c} {f : b ⟿ c} {g : a ⟿ b} →
                    fmapʰ {a} {c} (f ∘ g) ≡ fmapʰ {b} {c} f ∘ₛ fmapʰ {a} {b} g
        fmapʰ-dist {_} {_} {_} {f} {g} = extensionality (Cat.associativity C f g)

    module Yoneda
      {o}
      {hom : Hom o l}
      (C : Cat hom)
      (recF : Functor C 𝕊𝕖𝕥₀)
      (r : Set o)
      where
        {- hom-set of C -}
        _⟿_ = hom
        infix 5 _⟿_

        F = Functor.F recF
        fmapᶠ = Functor.fmap recF
        fmapᶠ-id = Functor.fmap-id recF

        fmapʰ = Functor.fmap (homF C r)

        {- construction of Yoneda map ⟹ -}
        map-⟹ : (∀ (a : Set o) → (r ⟿ a) →₀ F a) → F r
        map-⟹ Nat = Nat r (Cat.id C)

        {- construction of Yoneda map ⟸ -}
        map-⟸ : F r → (∀ (a : Set o) → (r ⟿ a) →₀ F a)
        map-⟸ x a k = fmapᶠ k x

        module Lemma
          (naturality : ∀ {r : Set o} → Naturality (homF C r) recF)
          where
            _∘_ : ∀ {x y z} {a : Set x} {b : Set y} {c : Set z} → (b → c) → (a → b) → (a → c)
            _∘_ f g x = f (g x)

            {- proof: composition of Yoneda map (⟹ ∘ ⟸) is identity -}
            id-right-left : map-⟹ ∘ map-⟸ ≡ (λ x → x)
            id-right-left = fmapᶠ-id

            {- proof: composition of Yoneda map (⟸ ∘ ⟹) is identity, arguments applied form -}
            id-left-right-applied : ∀ (Nat : ∀ (a : Set o) → (r ⟿ a) →₀ F a) (b : Set o) (k : r ⟿ b) →
                                    (map-⟸ ∘ map-⟹) Nat b k ≡ Nat b k
            id-left-right-applied Nat b k = trans naturality-on-id nat-on-right-id-k
              where
                id = Cat.id C

                naturality-on-id : (fmapᶠ {r} {b} k ∘ₛ Nat r) id ≡ (Nat b ∘ₛ fmapʰ {r} {b} k) id
                naturality-on-id = sym (cong-app (naturality Nat k) id)

                nat-on-right-id-k : (Nat b ∘ₛ fmapʰ {r} {b} k) id ≡ Nat b k
                nat-on-right-id-k = cong (Nat b) (Cat.right-id C k)

            {- proof: composition of Yoneda map (⟸ ∘ ⟹) is identity -}
            id-left-right : (map-⟸ ∘ map-⟹) ≡ Cat.id 𝕊𝕖𝕥
            id-left-right =
              extensionality λ Nat →
                extensionality-Nat Nat λ b →
                  extensionality (id-left-right-applied Nat b)
              where
                extensionality-Nat : ∀ (Nat : ∀ (a : Set o) → (r ⟿ a) →₀ F a) →
                                     (∀ (b : Set o) → (map-⟸ ∘ map-⟹) Nat b ≡ Nat b) →
                                     (map-⟸ ∘ map-⟹) Nat ≡ Nat
                extensionality-Nat Nat forallEQ =
                  extensionality
                    {_} {_}
                    {Set o} {λ (b : Set o) → (r ⟿ b) →₀ F b}
                    {(map-⟸ ∘ map-⟹) Nat} {Nat} forallEQ

            {- Since we have shown id-right-left , id-left-right , proof of Yoneda lemma is complete -}

    module WithCategory
      {o}
      {hom : Hom o l}
      (C : Cat hom)
      where
        _⟿_ = hom
        _⟿ᵒᵖ_ = get-homᵒᵖ _⟿_
        infix 5 _⟿_ _⟿ᵒᵖ_

        {- only hom term -}
        yonedaEmbeddingHom : {r s : Set o} →
                             (r ⟿ s)     →
                             (∀ (a : Set o) → (r ⟿ᵒᵖ a) → (s ⟿ᵒᵖ a))
        yonedaEmbeddingHom {r} {s} = Yoneda.map-⟸ (C ᵒᵖ) hom-s⟿ᵒᵖ r
          where
            hom-s⟿ᵒᵖ : Functor (C ᵒᵖ) 𝕊𝕖𝕥₀
            hom-s⟿ᵒᵖ = homF (C ᵒᵖ) s
            s⟿ᵒᵖ =  Functor.F hom-s⟿ᵒᵖ

        {- also known as Yoneda Functor -}
        yonedaEmbeddingHomᵒᵖ : {r s : Set o} →
                                (r ⟿ᵒᵖ s)  →
                                (∀ (a : Set o) → (r ⟿ a) → (s ⟿ a))
        yonedaEmbeddingHomᵒᵖ {r} {s} = Yoneda.map-⟸ C hom-s⟿ r
          where
            hom-s⟿ : Functor C 𝕊𝕖𝕥₀
            hom-s⟿ = homF C s
            s⟿ =  Functor.F hom-s⟿

    {- category to category function -}
    yonedaEmbedding : ∀ {o} {hom : Hom o l} (C : Cat hom) →
                      ∃ (λ (hom₁ : Hom o (l ⊔ lsuc o)) → Cat hom₁)
    yonedaEmbedding {o} {hom} C =
      _⟿₁_ ,
      record
      { id = id₁
      ; compose = _∘₁_
      ; left-id = left-id₁
      ; right-id = right-id₁
      ; associativity = associativity₁
      }
      where
        _⟿ᵒᵖ_ = get-homᵒᵖ hom
        infix 5 _⟿ᵒᵖ_

        _⟿₁_ : Set o -> Set o -> Set (l ⊔ lsuc o)
        r ⟿₁ s = ∀ (a : Set o) → (r ⟿ᵒᵖ a) → (s ⟿ᵒᵖ a)
        infix 5 _⟿₁_

        id₁ : ∀ {a} → a ⟿₁ a
        id₁ = λ a z → z

        _∘₁_ : ∀ {q r s} → (r ⟿₁ s) → (q ⟿₁ r) → (q ⟿₁ s)
        _∘₁_ f g a k = f a (g a k)
        infixr 9  _∘₁_

        left-id₁ : ∀ {a b} (f : a ⟿₁ b) → id₁ ∘₁ f ≡ f
        left-id₁ f = refl

        right-id₁ : ∀ {a b} (f : a ⟿₁ b) → f ∘₁ id₁ ≡ f
        right-id₁ f = refl

        associativity₁ : ∀ {a b c d} (f : c ⟿₁ d) (g : b ⟿₁ c) (h : a ⟿₁ b) →
                         (f ∘₁ g) ∘₁ h ≡ f ∘₁ (g ∘₁ h)
        associativity₁ f g h = refl

    {- also known as Yoneda Functor, essentially same as yonedaEmbedding function -}
    yonedaEmbeddingᵒᵖ : ∀ {o} {homᵒᵖ : Hom o l} (Cᵒᵖ : Cat homᵒᵖ) →
                        ∃ (λ (hom₁ : Hom o (l ⊔ lsuc o)) → Cat hom₁)
    yonedaEmbeddingᵒᵖ Cᵒᵖ = yonedaEmbedding Cᵒᵖ

    {- constructing Functor using yonedaEmbeddingᵒᵖ -}
    yonedaFunctor : ∀ {o} {homᵒᵖ : Hom o l} (Cᵒᵖ : Cat homᵒᵖ) →
                    Functor Cᵒᵖ (proj₂ (yonedaEmbeddingᵒᵖ Cᵒᵖ))
    yonedaFunctor {o} {homᵒᵖ} Cᵒᵖ =
      record
      { F = Y
      ; fmap = fmapʸ
      ; fmap-id = fmapʸ-id
      ; fmap-dist = fmapʸ-dist
      }
      where
        _⟿ᵒᵖ_ = homᵒᵖ
        infix 5 _⟿ᵒᵖ_

        idᵒᵖ = Cat.id Cᵒᵖ
        _∘ᵒᵖ_ = Cat.compose Cᵒᵖ
        infixr 9  _∘ᵒᵖ_

        _⟿ʸ_ : Hom o (l ⊔ lsuc o)
        r ⟿ʸ s = ∀ (a : Set o) → (a ⟿ᵒᵖ r) → (a ⟿ᵒᵖ s)
        infix 5 _⟿ʸ_

        Yc : Cat _⟿ʸ_
        Yc = proj₂ (yonedaEmbeddingᵒᵖ Cᵒᵖ)
        _∘ʸ_ = Cat.compose Yc
        infixr 9  _∘ʸ_

        idʸ : ∀ {a} → a ⟿ʸ a
        idʸ = λ a z → z

        Y : Set o → Set o
        Y a = a

        fmapʸ : ∀ {r s} → (r ⟿ᵒᵖ s) → (Y r ⟿ʸ Y s)
        fmapʸ {r} {s} f a g = f ∘ᵒᵖ g

        fmapʸ-id : ∀ {r} → fmapʸ {r} {r} idᵒᵖ ≡ idʸ
        fmapʸ-id = extensionality λ a → extensionality (Cat.left-id Cᵒᵖ)

        fmapʸ-dist : ∀ {q r s} {f : r ⟿ᵒᵖ s} {g : q ⟿ᵒᵖ r} →
                     fmapʸ {q} {s} (f ∘ᵒᵖ g) ≡ fmapʸ {r} {s} f ∘ʸ fmapʸ {q} {r} g
        fmapʸ-dist {_} {_} {_} {f} {g} =
          extensionality λ a →
            extensionality λ h →
              Cat.associativity Cᵒᵖ f g h