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


record iproduct {a} (I : Set a)  ( pi0 : I → Set a ) : Set a where
    field
       pi1 : ( i : I ) → pi0 i

open iproduct

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₂

≡-cong = Relation.Binary.PropositionalEquality.cong 


SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) 
     → IProduct ( Sets  {  c₂} ) I
SetsIProduct I fi = record {
       ai =  fi
       ; iprod = iproduct I fi
       ; pi  = λ i prod  → pi1 prod i
       ; isIProduct = record {
              iproduct = λ {q} qi x → record { pi1 = λ i → (qi i) x  }
            ; pif=q = pif=q
            ; ip-uniqueness = ip-uniqueness
            ; ip-cong  = ip-cong
       }
   } where
       iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
       iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x  }
       pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ]
       pif=q {q} qi {i} = refl
       ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
       ip-uniqueness = refl
       ipcx : {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x
       ipcx {q} {qi} {qi'} qi=qi x  = 
              begin
                record { pi1 = λ i → (qi i) x  }
             ≡⟨ ≡-cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡-cong ( λ f → f x )  (qi=qi i)  )) ⟩
                record { pi1 = λ i → (qi' i) x  }
             ∎  where
                  open  import  Relation.Binary.PropositionalEquality 
                  open ≡-Reasoning 
       ip-cong  : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1  qi' ]
       ip-cong {q} {qi} {qi'} qi=qi  = extensionality Sets ( ipcx qi=qi )




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₂ }  ( I   : Set  c₂ )    : Set  c₂ where
   field
     obj :  I

open ΓObj

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

open ΓMap

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

Γ :  { c₂ : Level } → Functor  (Sets { c₂}) (Sets { c₂}) 
Γ { c₂} =   record { FObj =  ΓObj ; FMap = ( λ f →  map (fmap f )) ; isFunctor = record {
         identity =  λ {b} → refl ;
         distr = λ {a} {b} {c} {f} {g} → refl ;
         ≈-cong = cong1
    } } where
       cong1 :  {A B : Obj Sets} {f g : Hom Sets A B} → Sets [ f ≈ g ] → Sets [ map (fmap f) ≈ map (fmap g) ]
       cong1 refl =  refl 


record Slimit  { c₂ } (I :  Set  c₂)  ( sobj : I → Set  c₂ ) (smap :  { a b  :   Set  c₂ } ( f : a → b ) →  Set  c₂ ) 
           : Set  c₂ where
    field 
        sm : I → I
        s-t0 : (i : I ) → sobj i

open Slimit

SetsLimit :  { c₂ : Level}  →  Limit Sets Sets Γ
SetsLimit { c₂}  = record { 
           a0 =  Slimit (Obj Sets) {!!} ΓMap
         ; t0 = record { 
               TMap = λ i → λ lim → s-t0 lim {!!}
             ; isNTrans = record { commute = {!!} } 
           }
         ; isLimit = record {
               limit  = {!!}
             ; t0f=t = {!!}
             ; limit-uniqueness  = {!!}
           }
       }  where
--           comm1 :  {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → s-t0 lim ? ) ] ≈
--                        Sets [ (λ lim → s-t0 lim ?) o FMap (K Sets Sets (Slimit (Obj Sets) ΓObj (λ {a} {b} → ΓMap))) f ] ]
  --           comm1 {a} {b} {f} = {!!}