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

natf :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
    →  { F G : Functor A B }
    → Functor A B  → Functor A (F ↓ G) → Functor A B
natf   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } {F} {G} H I = nat-f H I
         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

YonedaFpreserveLimit0 : {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))
YonedaFpreserveLimit0 {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
             ∎  ))


YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
       (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) 
YonedaFpreserveLimit A I b = record {
       preserve = λ Γ lim → YonedaFpreserveLimit0 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 =  λ f → unique 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 and U preserve limit then U is representable

open SmallFullSubcategory
open PreInitial

-- if U preserve limit,  K{*}↓U has initial object from freyd.agda

≡-cong = Relation.Binary.PropositionalEquality.cong


ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
   → Hom Sets (FObj (K Sets A *) b) (FObj U b)
ub A U b x OneObj = x
ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
   → Obj ( K Sets A * ↓ U)
ob A U b x = record { obj = b ; hom = ub A U b x}
fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )  {a b : Obj A} (f : Hom A a b) (x : FObj U a )
   → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) )
fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
  where
        fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U 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 U a x) ] ≈ Sets [ hom (ob A U 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 U a x) ] ) y 
             ≡⟨⟩
                FMap U f ( hom (ob A U a x) y )
             ≡⟨⟩
                FMap U f ( ub A U a x y )
             ≡⟨ fArrowComm1 a b f x y ⟩
                ub A U b (FMap U f x) y
             ≡⟨⟩
                hom (ob A U b (FMap U f x)) y
             ∎ ) where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning


-- if K{*}↓U has initial Obj, U is representable

UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
     (U : Functor A (Sets {c₂}) )
     ( i : Obj ( K (Sets) A * ↓ U) )
     (In : HasInitialObject ( K (Sets) A * ↓ U) i ) 
       → Representable A U (obj i)
UisRepresentable A U i In = record {
        repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
        ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
        ; reprId→  = iso→ 
        ; reprId←  = iso←
   } where
      comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
         ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y   
           ≡ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
      comm11 a b f y = begin
               ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y   
             ≡⟨⟩
                 A [ f o arrow (initial In (ob A U a y)) ]
             ≡⟨⟩
                 A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ]
             ≡⟨  ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y  o initial In (ob A U a y)] ) ) ⟩
                arrow (initial In (ob A U b (FMap U f y) ))
             ≡⟨⟩
                (Sets [ ( λ x → arrow (initial In (ob A U 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 i)) b)
      tmap1 b x = arrow ( initial In (ob A U b x ) ) 
      comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) 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 i)) f o tmap1 a 
             ≈⟨⟩
                FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob A U a x )))  
             ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
                ( λ x → arrow (initial In (ob A U 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 i) a ) → 
          (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡
                (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → A [ f o x ] ) ] )  y
      comm21 a b f y = begin
                FMap U f ( FMap U y (hom i OneObj))
             ≡⟨ ≡-cong ( λ k → k (hom i OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
                (FMap U (A [ f o y ] ) ) (hom i OneObj) 
             ∎  where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning
      tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj i)) b) (FObj U b)
      tmap2 b x =  ( FMap U x ) ( hom i 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 i)) 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 i OneObj ) )
             ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩
                ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → A [ f o x  ]  )
             ≈⟨⟩
                ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f 
             ≈⟨⟩
                tmap2 b o FMap (Yoneda A (obj i)) f 
             ∎
      iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * )
         → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z 
      iso0 x y  OneObj = refl
      iso→  : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ]
      iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin
               ( Sets [ tmap1 x o tmap2 x ] ) y
             ≈⟨⟩
                arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) ))) 
             ≈↑⟨  uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) }  ) ⟩
               y
             ∎  ))
      iso←  : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ]
      iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin 
               ( Sets [ tmap2 x o tmap1 x ] ) y
             ≡⟨⟩
               ( FMap U ( arrow ( initial In (ob A U x y ) ))  ) ( hom i OneObj )
             ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob A U x y ) )) ⟩
                 hom (ob A U x y) OneObj
             ≡⟨⟩
               y
             ∎  ) ) where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning