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

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 )

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

data OneMor {c : Level} : OneObject {c} → OneObject {c} → Set c where
  OneIdMor : OneMor OneObj OneObj

comp : {A B C : OneObject} → OneMor B C → OneMor A B → OneMor A C 
comp OneIdMor OneIdMor = OneIdMor

OneEquiv : {c : Level} {A B : OneObject {c} } → IsEquivalence {c} {c} {OneMor A B} _≡_
OneEquiv = record { refl = refl  ; sym = ≡-sym; trans = ≡-trans}

OneID : {A : OneObject} → OneMor A A
OneID {OneObj} = OneIdMor

OneAssoc : {A B C D : OneObject} {f : OneMor C D} {g : OneMor B C } {h : OneMor A B}
           → comp f (comp g h) ≡ comp (comp f g) h 
OneAssoc {OneObj} {OneObj} {OneObj} {OneObj} {OneIdMor} {OneIdMor} {OneIdMor} = refl

OneIdentityL : {A B : OneObject} {f : OneMor A B} → (comp OneID f) ≡ f
OneIdentityL {OneObj} {OneObj} {OneIdMor} = refl 

OneIdentityR : {A B : OneObject} {f : OneMor A B} → (comp f OneID) ≡ f
OneIdentityR {OneObj} {OneObj} {OneIdMor} = refl 

o-resp-≡ : {A B C : OneObject} {f g : OneMor A B} {h i : OneMor B C} → f ≡ g → h ≡ i → comp h f ≡ comp i g
o-resp-≡ {OneObj} {OneObj} {OneObj} {f} {g} {h} {i} f≡g h≡i =
  ≡-trans (cong (comp h) f≡g) (cong (λ x → comp x g) h≡i)


isCategory : { c : Level } → IsCategory {c} {c} {c} OneObject OneMor _≡_ comp OneID
isCategory = record { isEquivalence = OneEquiv
                    ; identityL = OneIdentityL
                    ; identityR = OneIdentityR
                    ; o-resp-≈ = o-resp-≡
                    ; associative = OneAssoc
                    }

ONE : { c : Level } → Category c c c
ONE = record { Obj = OneObject
             ; Hom = OneMor
             ; _≈_ = _≡_ 
             ; Id  = OneID
             ; isCategory = isCategory
             }

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

open import freyd
open SmallFullSubcategory
open Complete
open PreInitial
open HasInitialObject
open import Comma
open CommaObj
open CommaHom

KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
      (a : Obj A )
      → HasInitialObject {c₁} {c₂} {ℓ}  ( K Sets ONE OneObject ↓ (Yoneda A a) ) ( record  { obj = OneObj ; hom = {!!} } )
KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
           initial =  λ b → initial0 b
         ; uniqueness =  {!!}
     } where
         commaCat : Category  (c₂ ⊔ c₁) c₂ ℓ
         commaCat = K Sets ONE OneObject ↓ Yoneda A a
         initObj  : Obj (K Sets ONE OneObject ↓ Yoneda A a)
         initObj = record { obj = OneObj ; hom = {!!} }
         initial0comm1 :  (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) → (x :  {!!} )
            →  FMap (Yoneda A a) (hom b {!!}) x ≡ hom b {!!}
         initial0comm1 b x =  let open ≈-Reasoning A in ≈-≡ A ( begin
               FMap (Yoneda A a) (hom b {!!}) x  
             ≈⟨⟩
               hom b {!!} o x
             ≈⟨ {!!} ⟩
               hom b {!!}
             ∎ )
         initial0comm :  (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) →
            Sets [ Sets [ FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a) ] ≈ {!!} ]
         initial0comm b = let open ≈-Reasoning Sets in begin
                   FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a) 
             ≈⟨ {!!} ⟩
                    {!!}
             ∎ 
         initial0 : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) →
            Hom (K Sets ONE OneObject ↓ (Yoneda A a)) initObj b
         initial0 b = record {
                arrow = {!!}
              ; comm = {!!} }
            

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

open SmallFullSubcategory
open PreInitial
--  
-- UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
--       (U : Functor A (Sets {c₂}) )
--       (a : Obj (Sets {c₂})) (ax : a)
--       (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) )  
--       (PI : PreInitial {c₁} {c₂} {ℓ} ( K Sets ONE OneObject ↓ U) (SFSF SFS )) 
--         → Representable A U (obj (preinitialObj PI ))
-- UisRepresentable A U a ax SFS PI = record {
--          repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } }
--          ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = {!!} } }
--          ; reprId→  = λ {y}  →　?
--          ; reprId←  = λ {y}  →　?
--     } where
--        tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b)
--        tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) )
--        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 ) ax )