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 Slimit  { c₂ } ( ΓObj :  Obj (Sets { c₂ }) → Obj (Sets { c₂ }) ) ( ΓMap :  {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj A) ( ΓObj B )) 
      : Set  c₂ where
     -- field
        -- tlimit : Obj Sets
        --  tmap :  (A : Obj Sets) → Hom Sets ? (ΓObj A)
        -- tcommute :   {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap  b o id1 Sets tlimit  ] ]

open Slimit

SetsLimit : { c₂ : Level} 
          ( ΓObj :  Obj Sets → Obj Sets ) ( ΓMap :  {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj A) ( ΓObj B ))
          ( Γ : IsFunctor  (Sets { c₂}) (Sets { c₂}) ΓObj ΓMap ) 
        →  Limit Sets Sets ( record { FObj =  ΓObj ; FMap =  ΓMap ; isFunctor = Γ } )
SetsLimit { c₂} ΓObj ΓMap Γ = record { 
           a0 =  Slimit  ΓObj  ΓMap
         ; t0 = record { TMap = tmap ; isNTrans = record { commute = tcommute } }
         ; isLimit = record {
               limit  = {!!}
             ; t0f=t = {!!}
             ; limit-uniqueness  = {!!}
           }
       } where
          tmap :  (a : Obj Sets) → Hom Sets (Slimit  ΓObj  ΓMap) (ΓObj a)
          tmap  a _ = {!!}
          tcommute :   {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap  b o id1 Sets (Slimit  ΓObj  ΓMap)  ] ]
          tcommute {a} {b} {f} = {!!}