open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
open import Category.Sets

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,-)
--

-- A is Locally small
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 co Yoneda Functor
--
----

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

HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
HomA  {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 ]
             ∎ )


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

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

         repr→ : NTrans A (Sets {c₂}) U (HomA A b )
         repr← : NTrans A (Sets {c₂}) (HomA A b)  U
         representable→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
         representable←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]

-- HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →  (b : Obj A)
--       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
--       → LimitPreserve A I (Sets  {c₂}) ( HomA A b )
-- HpreseveLimit {_} { c₂} A b I =  record {
--        preserve = λ Γ limita → record {
--              limit = λ a t → limitu a Γ t limita
--              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
--              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
--        }
--    } where
--       limitu :   ( a : Obj Sets ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
--           Hom Sets a (FObj (HomA A b) (a0 limita))
--       limitu  = {!!}
--       t0f=tu :    { a : Obj  Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
--            ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ]
--       t0f=tu  = {!!}
--       limit-uniquenessu :    { a : Obj Sets } → (Γ : Functor I A ) 
--            →   ( limita : Limit A I Γ  ) →
--           ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f :  Hom Sets a (FObj (HomA A b) (a0 limita)) ) 
--            →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) )
--            →  Sets [ limitu a Γ t limita ≈ f ]
--       limit-uniquenessu = {!!}



--
-- 
-- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)
--       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
--      ( rep :  Representable A U b ) → LimitPreserve A I (Sets  {c₂}) U 
-- UpreseveLimit {_} { c₂} A U b I rep =  record {
--        preserve = λ Γ limita → record {
--              limit = λ a t → limitu a Γ t limita
--              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
--              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
--        }
--    } where
--       limitu :   ( a : Obj (Sets  {c₂}) ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
--           Hom Sets a (FObj U (a0 limita))
--       limitu  = {!!}
--       t0f=tu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
--            ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ]
--       t0f=tu  = {!!}
--       limit-uniquenessu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) 
--            →   ( limita : Limit A I Γ  ) →
--           ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f :  Hom Sets a (FObj U (a0 limita)) ) 
--            →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) )
--            →  Sets [ limitu a Γ t limita ≈ f ]
--       limit-uniquenessu = {!!}
--