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

module SetsCompleteness where


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

record Σ {a} (A : Set a) (B : Set a) : Set a where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B 

open Σ public


SetsProduct :  {  c₂ : Level} → CreateProduct ( Sets  {  c₂} )
SetsProduct { c₂ } = record { 
         product =  λ a b →    Σ a  b
       ; π1 = λ a b → λ ab → (proj₁ ab)
       ; π2 = λ a b → λ ab → (proj₂ ab)
       ; isProduct =  λ a b → record {
              _×_  = λ f g  x →   record { proj₁ = f  x ;  proj₂ =  g  x }     -- ( f x ,  g x ) 
              ; π1fxg=f = refl
              ; π2fxg=g  = refl
              ; uniqueness = refl
              ; ×-cong   =  λ {c} {f} {f'} {g} {g'} f=f g=g →  prod-cong a b f=f g=g
          }
      } where
          prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b }
              → Sets [ f ≈ f' ] → Sets [ g ≈ g' ]
              → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
          prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl


SetsEqualizer :  {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g
SetsEqualizer f g = record { 
           equalizer-c = {!!} 
         ; equalizer = {!!}
         ; isEqualizer = record {
               fe=ge  = {!!}
             ; k = {!!}
             ; ek=h = {!!}
             ; uniqueness  = {!!}
           }
       }

open Functor
open NTrans

record ΓObj   { c₂ }  (x :  Set  c₂ ) : Set  c₂ where
   field
     obj :  x

open ΓObj

record ΓMap   { c₂ }  {a b :  Set  c₂ } ( f : a → b )  : Set  c₂ where
   field
     map : ΓObj a → ΓObj b

open ΓMap


record Slimit  { c₂ }  ( sobj : Set  c₂ →  Set  c₂ ) (smap :  {a b :  Set  c₂ } ( f : a → b ) →  Set  c₂ )
           : Set  c₂ where
--    field 
--       aap : ΓObj slim  
--       ap : ΓObj slim  → ΓObj slim
--       hoge : sobj  slim
--       hoge1 : smap {slim} {slim} ( λ x → x )

record ΓTMap   { c₂ }  (a :  Set  c₂ )   : Set  c₂ where
   field
     tmap : a →  Slimit  ΓObj  ΓMap → ΓObj a

open ΓTMap


--       sobj  :  S
--       smap  :  fobj  S
--       hoge  :  ΓObj S

--        bb :  ΓObj  I
--        cc :  I → I

open Slimit

tmp : { c₂ : Level}   {a b :  Set  c₂ } → (f : a → b  ) → ΓMap f
tmp {a} {b} f =  record { map = λ aobj →  record { obj = f ( obj aobj ) } }

ttmp : {c₂ : Level}   (A  :  Set  c₂ ) →   ΓTMap A
ttmp  A = record { tmap  =  λ a slim → record { obj = a } }

SetsLimit :  { c₂ : Level} (e : Set  c₂)   ( Γ : IsFunctor  (Sets { c₂}) (Sets { c₂}) ΓObj ( λ f →  map (tmp f ) ))
        →  Limit Sets Sets ( record { FObj =  ΓObj ; FMap = ( λ f →  map (tmp f )) ; isFunctor = Γ } )
SetsLimit { c₂} e   Γ = record { 
           a0 =  Slimit   ΓObj  ΓMap  
         ; t0 = record { TMap = λ i → {!!} ; isNTrans = record { commute = {!!} } }
         ; isLimit = record {
               limit  = {!!}
             ; t0f=t = {!!}
             ; limit-uniqueness  = {!!}
           }
       } where  
            tmap0 :  (a : Obj Sets) → Hom Sets (FObj (K Sets Sets (  Slimit   ΓObj  ΓMap)) a) (ΓObj a)
            tmap0 a oa =  tmap ( ttmp a ) ? oa