open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
open import Category.Sets renaming ( _o_ to _*_ )

module freyd2 
   where

open import HomReasoning
open import cat-utility
open import Relation.Binary.Core
open import Function

----------
--
--    a : Obj A
--    U : A → Sets
--    U ⋍ Hom (a,-)
--

-- maybe this is a part of local smallness
postulate ≈-≡ :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y

import Relation.Binary.PropositionalEquality
-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂


----
--
--  Hom ( a, - ) is Object mapping in Yoneda Functor
--
----

open NTrans 
open Functor
open Limit
open IsLimit
open import Category.Cat

Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
Yoneda  {c₁} {c₂} {ℓ} A a = record {
    FObj = λ b → Hom A a b
  ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ]    --   f : Hom A x y  → Hom Sets (Hom A a x ) (Hom A a y)
  ; isFunctor = record {
             identity =  λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ;
             distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
             ≈-cong = λ eq → extensionality A ( λ x →  lemma-y-obj3 x eq ) 
        } 
    }  where
        lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) →  A [ id1 A b o x ] ≡ x
        lemma-y-obj1 {b} x = let open ≈-Reasoning A  in ≈-≡ A idL
        lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ 
               A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin
               A [ A [ g o f ] o x ]
             ≈↑⟨ assoc ⟩
               A [ g o A [ f o x ] ]
             ≈⟨⟩
               ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
             ∎ )
        lemma-y-obj3 :  {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] →   A [ f o x ] ≡ A [ g o x ]
        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning A in ≈-≡ A ( begin
                A [ f o x ]
             ≈⟨ resp refl-hom eq ⟩
                A [ g o x ]
             ∎ )

-- Representable  U  ≈　Hom(A,-)

record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
   field
         -- FObj U x  :  A  → Set
         -- FMap U f  =  Set → Set (locally small)
         -- λ b → Hom (a,b) :  A → Set
         -- λ f → Hom (a,-) = λ b → Hom  a b    

         repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
         repr← : NTrans A (Sets {c₂}) (Yoneda A a)  U
         reprId→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )]
         reprId←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]

open Representable
open import freyd

_↓_ :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
    →  ( F G : Functor A B )
    →  Category  (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
_↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } F G  = CommaCategory
         where open import Comma1 F G

open import freyd
open SmallFullSubcategory
open Complete
open PreInitial
open HasInitialObject
open import Comma1
open CommaObj
open LimitPreserve

-- Representable Functor U preserve limit , so K{*}↓U is complete
--
--    Yoneda A b =  λ a → Hom A a b    : Functor A Sets
--                                     : Functor Sets A

UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
      (b : Obj A ) 
      (Γ : Functor I A) (limita : Limit A I Γ) →
        IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b))
UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record {
         limit = λ a t → ψ a t
       ; t0f=t = λ {a t i} → t0f=t0 a t i
       ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t 
    } where 
      hat0 :  NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ)
      hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)
      haa0 : Obj Sets
      haa0 = FObj (Yoneda A b) (a0 lim)
      ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ
      ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where
         commute1 :  {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} →
                A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ]  ]
         commute1  {a₁} {b₁} {f} = let open ≈-Reasoning A in begin
                 FMap Γ f o TMap t a₁ x
             ≈⟨⟩
                 ( ( FMap (Yoneda A b  ○ Γ ) f )  *  TMap t a₁ ) x
             ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩
                 ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x
             ≈⟨⟩
                 ( TMap t b₁ * id1 Sets a ) x
             ≈⟨⟩
                 TMap t b₁ x 
             ≈↑⟨ idR ⟩
                 TMap t b₁ x o id1 A b
             ≈⟨⟩
                 TMap t b₁ x o FMap (K A I b) f 
             ∎ 
      ψ  :  (X : Obj Sets)  ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ))
          →  Hom Sets X (FObj (Yoneda A b) (a0 lim))
      ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
      t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I)
           → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ]
      t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
                 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t  ] ) x
             ≈⟨⟩
                FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
             ≈⟨⟩ -- FMap (Hom A b ) f g  = A [ f o g  ]
                TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b )
             ≈⟨  cdr idR ⟩
                TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) 
             ≈⟨  t0f=t (isLimit lim) ⟩
                TMap (ta a x t) i
             ≈⟨⟩
                 TMap t i x
             ∎  ))
      limit-uniqueness0 :  {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} →
        ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) →
        Sets [ ψ a t ≈ f ]
      limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
                  ψ a t x
             ≈⟨⟩
                 FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )
             ≈⟨⟩
                 limit (isLimit lim) b (ta a x t ) o id1 A b 
             ≈⟨ idR ⟩
                 limit (isLimit lim) b (ta a x t ) 
             ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩
                  f x
             ∎  ))


UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
       (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) 
UpreserveLimit A I b = record {
       preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
   } 


-- K{*}↓U has preinitial full subcategory if U is representable
--     if U is representable,  K{*}↓U has initial Object ( so it has preinitial full subcategory )

open CommaHom

data * {c : Level} : Set c where
  OneObj : *

KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
      (a : Obj A )
      → HasInitialObject  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
           initial =  λ b → initial0 b
         ; uniqueness =  λ b f → unique b f
     } where
         commaCat : Category  (c₂ ⊔ c₁) c₂ ℓ
         commaCat = K Sets A * ↓ Yoneda A a
         initObj  : Obj (K Sets A * ↓ Yoneda A a)
         initObj = record { obj = a ; hom = λ x → id1 A a }
         comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] )  x ≡ hom b x
         comm2 b OneObj = let open ≈-Reasoning A in  ≈-≡ A ( begin
                ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj
             ≈⟨⟩
                FMap (Yoneda A a) (hom b OneObj) (id1 A a)
             ≈⟨⟩
                hom b OneObj o id1 A a
             ≈⟨ idR ⟩
                hom b OneObj 
             ∎  )
         comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ]
         comm1 b = let open ≈-Reasoning Sets in begin
                FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a )
             ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩
                hom b 
             ≈⟨⟩
                hom b o FMap (K Sets A *) (hom b OneObj) 
             ∎ 
         initial0 : (b : Obj commaCat) →
            Hom commaCat initObj b
         initial0 b = record {
                arrow = hom b OneObj
              ; comm = comm1 b }
         -- what is comm f ?
         comm-f :  (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
            → Sets [ Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ]
               ≈ Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ] 
         comm-f b f = comm f
         unique : (b : Obj (K Sets A * ↓ Yoneda A a))  (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
                → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ]
         unique b f = let open ≈-Reasoning A in begin
                arrow f
             ≈↑⟨ idR ⟩
                arrow f o id1 A a
             ≈⟨⟩
                ( Sets [ FMap  (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a)  ] ) (id1 A a)
             ≈⟨⟩
               ( Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj
             ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩
               ( Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ) OneObj
             ≈⟨⟩
                hom b OneObj
             ∎ 

            

-- A is complete and K{*}↓U has preinitial full subcategory then U is representable

open SmallFullSubcategory
open PreInitial

≡-cong = Relation.Binary.PropositionalEquality.cong

UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( comp : Complete A A )
     (U : Functor A (Sets {c₂}) )
     (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )  
     (PI : PreInitial ( K (Sets) A * ↓ U)  (SFSF SFS)) 
       → Representable A U (obj (preinitialObj PI ))
UisRepresentable A comp U SFS PI = record {
        repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
        ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
        ; reprId→  = {!!}
        ; reprId←  = {!!}
   } where
      pi : Obj ( K (Sets) A * ↓ U) 
      pi = preinitialObj PI
      pihom : Hom Sets (FObj (K Sets A *) (obj pi)) (FObj U (obj pi))
      pihom = hom pi
      ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
      ub b x OneObj = x
      ob : (b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U)
      ob b x = record { obj = b ; hom = ub b x}
      piArrow : (b : Obj ( K Sets A * ↓ U)) → Hom ( K Sets A * ↓ U) pi b
      piArrow b =  SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) b} )
      fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y
      fArrowComm1 a b f x OneObj = refl
      fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → 
         Sets [ Sets [ FMap U f o hom (ob a x) ] ≈ Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ]
      fArrowComm a b f x = extensionality Sets ( λ y → begin 
                ( Sets [ FMap U f o hom (ob a x) ] ) y 
             ≡⟨⟩
                FMap U f ( hom (ob a x) y )
             ≡⟨⟩
                FMap U f ( ub a x y )
             ≡⟨ fArrowComm1 a b f x y ⟩
                ub b (FMap U f x) y
             ≡⟨⟩
                hom (ob b (FMap U f x)) y
             ≡⟨⟩
                ( Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ) y
             ∎ ) where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning
      fArrow :  (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
      fArrow a b f x = record { arrow = f ; comm = fArrowComm a b f x }
      preinitComm : (a : Obj A ) ( x : FObj U a ) → Sets [ Sets [ FMap U (arrow (piArrow (ob a x))) o hom pi ]
         ≈ Sets [ ub a x  o FMap (K Sets A *) (arrow (piArrow (ob a x))) ] ]
      preinitComm a x = comm (piArrow (ob a x ))
      equ : {a b : Obj A} → (f g : Hom A a b)  → IsEqualizer A (equalizer-e comp f g ) f g
      equ f g = Complete.isEqualizer comp f g 
      ep : {a b : Obj A} → {f g : Hom A a b}  → Obj A 
      ep {a} {b} {f} {g} = equalizer-p comp f g
      ee :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ep {a} {b} {f} {g} ) a 
      ee {a} {b} {f} {g} = equalizer-e comp f g
      preinitialEqu : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y ) → 
          IsEqualizer A ee (A [ arrow f o arrow ( preinitialArrow PI {x}) ] ) ( arrow ( preinitialArrow PI {y}) ) 
      preinitialEqu {x} {y} f = Complete.isEqualizer comp ( A [ arrow f o arrow (preinitialArrow PI)  ] ) ( arrow ( preinitialArrow PI )) 
      pa : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y )
         → Hom ( K (Sets) A * ↓ U) (preinitialObj PI)
           (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} )
      pa {x} {y} f = piArrow (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} ) 
        --
        --         e             f
        --    c  -------→ a ---------→ b
        --    ^        .     ---------→
        --    |      .            g
        --    |k   .
        --    |  . h
        --    d
        --
      comm13 : (a b : Obj ( K Sets A * ↓ U)) (f : Hom ( K Sets A * ↓ U) a b )  → ( K Sets A * ↓ U) [
           ( K Sets A * ↓ U) [ f o preinitialArrow PI ]  ≈ preinitialArrow PI ]   
      comm13 a b f = let open ≈-Reasoning A in begin
                arrow ( ( K Sets A * ↓ U) [ f o preinitialArrow PI ] ) 
             ≈⟨⟩
                arrow f o arrow ( preinitialArrow PI {{!!}})
             ≈⟨ {!!} ⟩
                arrow ( preinitialArrow PI {{!!}} )
             ∎  
      comm12 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → ( K Sets A * ↓ U) [
          FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) ≈ FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) ] 
      comm12 a b f y = let open ≈-Reasoning ( K Sets A * ↓ U) in begin
                FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) 
             ≈⟨ {!!} ⟩
                FMap (SFSF SFS) ( fArrow a b f y ) o FMap (SFSF SFS) ( piArrow (ob a y)) 
             ≈⟨ {!!} ⟩
                FMap (SFSF SFS) ( fArrow a b f y ) o preinitialArrow PI {FObj (SFSF SFS) (ob a y ) }
             ≈⟨ comm13 (FObj (SFSF SFS) (ob a y)) (FObj (SFSF SFS) (ob b (FMap U f y))) (FMap (SFSF SFS) (fArrow a b f y)) ⟩
                preinitialArrow PI {FObj (SFSF SFS) (ob b (FMap U f y )) }
             ≈⟨ {!!} ⟩
                FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) 
             ∎ 
      comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
         ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y   
           ≡ (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
      comm11 a b f y = begin
               ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y   
             ≡⟨⟩
                 A [ f o arrow (piArrow (ob a y)) ]
             ≡⟨⟩
                 A [ arrow ( fArrow a b f y )  o arrow (piArrow (ob a y)) ]
             ≡⟨⟩
                arrow ( ( K Sets A * ↓ U) [ ( fArrow a b f y )  o (piArrow (ob a y)) ] )
             ≡⟨ {!!} ⟩
                arrow ( ( SFSFMap← SFS ) (  FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ ( fArrow a b f y )  o (piArrow (ob a y)) ] ) ) )
             ≡⟨ ≡-cong ( λ k → arrow ( (SFSFMap← SFS ) k ))  ( ≈-≡ ( K Sets A * ↓ U) ( comm12 a b f y ) ) ⟩
                arrow ( ( SFSFMap← SFS ) (  FMap (SFSF SFS) ( piArrow (ob b (FMap U f y) ) )) )
             ≡⟨ {!!} ⟩
                arrow (piArrow (ob b (FMap U f y) ))
             ≡⟨⟩
                (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
             ∎  where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning
      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
      tmap1 b x =  arrow ( piArrow ( ob b x ) )
      comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
      comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
                FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a 
             ≈⟨⟩
                FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow ( ob a x )))  
             ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
                ( λ x → arrow (piArrow (ob b x))) o FMap U f 
             ≈⟨⟩
                tmap1 b o FMap U f 
             ∎ 
      comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) → 
          (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡
                (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] )  y
      comm21 a b f y = begin
                FMap U f ( FMap U y (hom (preinitialObj PI) OneObj))
             ≡⟨ ≡-cong ( λ k → k (hom (preinitialObj PI) OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
                (FMap U (A [ f o y ] ) ) (hom (preinitialObj PI) OneObj) 
             ∎  where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning
      tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
      tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
      comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈
        Sets [ tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f ] ]
      comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin
                FMap U f o tmap2 a 
             ≈⟨⟩
                FMap U f o ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) )
             ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩
                ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o ( λ x → A [ f o x  ]  )
             ≈⟨⟩
                ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o FMap (Yoneda A (obj (preinitialObj PI))) f 
             ≈⟨⟩
                tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f 
             ∎