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
open import Data.Product


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 →  ( 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  = {!!}
           }
       }


SetsLimit : { c₁' c₂' ℓ' : Level} {  c₂ : Level}  ( I : Category c₁' c₂' ℓ' ) → ( Γ : Functor I (Sets { c₂}) ) →  Limit Sets I Γ
SetsLimit I Γ = record { 
           a0 = {!!} 
         ; t0 = {!!}
         ; isLimit = record {
               limit  = {!!}
             ; t0f=t = {!!}
             ; limit-uniqueness  = {!!}
           }
       }