{-# OPTIONS --without-K --safe #-}
module Categories.CoYoneda where

-- CoYoneda Lemma.  See Yoneda for more documentation

open import Level using (Level; _⊔_; lift; lower)
open import Function.Base using (_$_)
open import Function.Bundles using (Inverse; Func; _⟨$⟩_)
open import Relation.Binary.Bundles using (module Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR
open import Data.Product using (_,_; Σ)

open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Product using (πʳ; πˡ; _※_)
open import Categories.Category.Construction.Presheaves using (CoPresheaves)
open import Categories.Category.Construction.Functors using (eval)
open import Categories.Category.Construction.Functors using (Functors)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Hom using (module Hom; Hom[_][_,-]; Hom[_][-,-])
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Construction.LiftSetoids using (LiftSetoids)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.NaturalTransformation.Hom as NT-Hom

open Func

private
  variable
    o  e : Level

module Yoneda (C : Category o  e) where
  open Category C hiding (op) -- uses lots
  open HomReasoning using (_○_; ; refl⟩∘⟨_)
  open MR C using (id-comm)
  open NaturalTransformation using (η; commute; sym-commute)
  open NT-Hom C using (Hom[C,A]⇒Hom[C,B])
  private
    module CE = Category.Equiv C using (refl)
    module C = Category C using (op)

  -- The CoYoneda embedding functor
  embed : Functor C.op (CoPresheaves C)
  embed = record
    { F₀           = Hom[ C ][_,-]
    ; F₁           = Hom[C,A]⇒Hom[C,B] -- B⇒A induces a NatTrans on the Homs.
    ; identity     = identityʳ
    ; homomorphism = sym-assoc
    ; F-resp-≈     = λ f≈g  refl⟩∘⟨ f≈g
    }

  -- Using the adjunction between product and product, we get a kind of contravariant Bifunctor
  yoneda-inverse : (a : Obj) (F : Functor C (Setoids  e)) 
    Inverse (Category.hom-setoid (CoPresheaves C) {Functor.F₀ embed a} {F}) (Functor.F₀ F a)
  yoneda-inverse a F = record
    { to = λ nat  η nat a ⟨$⟩ id
    ; from = λ x  ntHelper record
        { η       = λ X  record
          { to = λ X⇒a  F.₁ X⇒a ⟨$⟩ x
          ; cong  = λ i≈j  F.F-resp-≈ i≈j
          }
        ; commute = λ {X} {Y} X⇒Y {f} 
          let module SR = SetoidR (F.₀ Y) in
          SR.begin
             F.₁ (X⇒Y  f  id) ⟨$⟩ x   SR.≈⟨ F.F-resp-≈ (∘-resp-≈ʳ identityʳ) 
             F.₁ (X⇒Y  f) ⟨$⟩ x        SR.≈⟨ F.homomorphism 
             F.₁ X⇒Y ⟨$⟩ (F.₁ f ⟨$⟩ x)
           SR.∎
        }
    ; to-cong = λ i≈j  i≈j
    ; from-cong = λ i≈j  cong (F.₁ _) i≈j
    ; inverse =
       ( λ {b} {nat} eq  
          let module SR = SetoidR (F.₀ a) in
          let open SR in begin
          to (η nat a) id ≈⟨ eq 
          to (F.₁ id) b    ≈⟨ F.identity 
           b                    )
       , λ {nat} {y} eq {b} {f} 
          let open Setoid (F.₀ b) in
          let module SR = SetoidR (F.₀ b) in
          let open SR in
          begin
            to (F.₁ f) y                 ≈⟨ cong (F.₁ f) eq 
            to (F.₁ f) (to (η nat a) id) ≈⟨ sym-commute nat f  
            to (η nat b) (f  id  id)   ≈⟨ cong (η nat b) (refl⟩∘⟨ identity²  identityʳ) 
            to (η nat b) f                
    }
    where
    module F = Functor F using (; ; F-resp-≈; homomorphism; identity)
    module SE = Setoid (F.₀ a)

  private
    Nat[Hom[C][c,-],F] : Bifunctor (CoPresheaves C) C (Setoids (o    e) (o    e))
    Nat[Hom[C][c,-],F] = Hom[ CoPresheaves C ][-,-] ∘F (Functor.op embed ∘F πʳ  πˡ)

    FC : Bifunctor (CoPresheaves C) C (Setoids _ _)
    FC = LiftSetoids (o    e) (o  ) ∘F eval {C = C} {D = Setoids  e}

    module yoneda-inverse {a} {F} = Inverse (yoneda-inverse a F)

  -- the two bifunctors above are naturally isomorphic.
  -- it is easy to show yoneda-inverse first then to yoneda.
  yoneda : NaturalIsomorphism Nat[Hom[C][c,-],F] FC
  yoneda = record
    { F⇒G = ntHelper record
      { η       = λ where
        (F , A)  record
          { to = λ α  lift (yoneda-inverse.to α)
          ; cong  = λ i≈j  lift i≈j
          }
      ; commute = λ where
        {_} {G , B} (α , f) {β}  lift $ cong (η α B) (helper f β)
      }
    ; F⇐G = ntHelper record
      { η       = λ { (F , A)  record
          { to = λ x  yoneda-inverse.from (lower x)
          ; cong  = λ i≈j  cong (Functor.F₁ F _) (lower i≈j)
          } }
      ; commute = λ { {F , A} {G , B} (α , f) {X} {Z} {h}  helper′ α f}
      }
    ; iso = λ { (F , A)  record
        { isoˡ = λ {α}  yoneda-inverse.strictlyInverseʳ α
        ; isoʳ = lift (Functor.identity F)
        } }
    }
    where helper : {F : Functor C (Setoids  e)}
                   {A B : Obj} (f : A  B)
                   (β : NaturalTransformation Hom[ C ][ A ,-] F) 
                   Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ id  f) (Functor.F₁ F f ⟨$⟩ (η β A ⟨$⟩ id))
          helper {F} {A} {B} f β = S.begin
            η β B ⟨$⟩ id  f        S.≈⟨ cong (η β B) (MR.id-comm-sym C  ∘-resp-≈ʳ ( identity²)) 
            η β B ⟨$⟩ f  id  id   S.≈⟨ commute β f 
            F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.∎
            where
            module F = Functor F using (;)
            module S = SetoidR (F.₀ B)

          helper′ :  {F G : Functor C (Setoids  e)}
                      {A B Z : Obj}
                      {h : B  Z}
                      {X : Setoid.Carrier (Functor.F₀ F A)}
                      (α : NaturalTransformation F G)
                      (f : A  B) 
                      Setoid._≈_ (Functor.F₀ G Z) (Functor.F₁ G h ⟨$⟩ (η α B ⟨$⟩ (Functor.F₁ F f ⟨$⟩ X)))
                                          (η α Z ⟨$⟩ (Functor.F₁ F (h  f) ⟨$⟩ X))
          helper′ {F} {G} {A} {B} {Z} {h} {X} α f = S.begin
            G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X))  S.≈˘⟨ commute α h 
            η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ X))  S.≈˘⟨ cong (η α Z) F.homomorphism 
            η α Z ⟨$⟩ (F.₁ (h  f) ⟨$⟩ X)       S.∎
            where
              module F = Functor F using (; ; homomorphism; F-resp-≈)
              module G = Functor G using (; )
              module S = SetoidR (G.₀ Z)

  module yoneda = NaturalIsomorphism yoneda