open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
open import Category.Sets renaming ( _o_ to _*_ )

module SetsCompleteness where


open import cat-utility
open import Relation.Binary.Core
open import Function
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 

≈-to-≡ :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
   Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
≈-to-≡ refl  x  = refl

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 sproduct {a} (I : Set a)  ( Product : I → Set a ) : Set a where
    field
       proj : ( i : I ) → Product i

open sproduct

iproduct1 : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (sproduct I fi)
iproduct1 I fi {q} qi x = record { proj = λ i → (qi i) x  }
ipcx : {  c₂ : Level} → (I : Obj (Sets {  c₂})) (fi : I → Obj Sets ) {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 I fi qi x ≡ iproduct1 I fi qi' x
ipcx I fi {q} {qi} {qi'} qi=qi x  = 
      begin
        record { proj = λ i → (qi i) x  }
     ≡⟨ ≡cong ( λ qi → record { proj = qi } ) ( extensionality Sets (λ i → ≈-to-≡  (qi=qi i) x )) ⟩
        record { proj = λ i → (qi' i) x  }
     ∎  where
          open  import  Relation.Binary.PropositionalEquality 
          open ≡-Reasoning 
ip-cong  : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 I fi qi ≈ iproduct1  I fi qi' ]
ip-cong I fi {q} {qi} {qi'} qi=qi  = extensionality Sets ( ipcx I fi qi=qi )

SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (fi : I → Obj Sets ) 
     → IProduct ( Sets  {  c₂} ) I
SetsIProduct I fi = record {
       ai =  fi
       ; iprod = sproduct I fi
       ; pi  = λ i prod  → proj prod i
       ; isIProduct = record {
              iproduct = iproduct1 I fi 
            ; pif=q = pif=q
            ; ip-uniqueness = ip-uniqueness
            ; ip-cong  = ip-cong I fi
       }
   } where
       pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj prod i) o iproduct1 I fi qi ] ≈ qi i ]
       pif=q {q} qi {i} = refl
       ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (sproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ]
       ip-uniqueness = refl


        --
        --         e             f
        --    c  -------→ a ---------→ b        f ( f' 
        --    ^        .     ---------→
        --    |      .            g
        --    |k   .
        --    |  . h
        --y : d

        -- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda

data sequ {c : Level} (A B : Set c) ( f g : A → B ) :  Set c where
    elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g

equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b  f g ) →  a
equ  (elem x eq)  = x 

fe=ge0  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →  
     (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
fe=ge0 (elem x eq )  =  eq

irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
irr refl refl = refl

elm-cong :  {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →   (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
elm-cong ( elem x eq  ) (elem .x eq' ) refl   =  ≡cong ( λ ee → elem x ee ) ( irr eq eq' )

fe=ge  : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} 
     →  Sets [ Sets [ f o (λ e → equ {_} {a} {b} {f} {g} e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
fe=ge  =  extensionality Sets (fe=ge0 ) 
k : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} (h : Hom Sets d a) 
     → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
k {_} {_} {_} {_} {_} {d} h eq = λ x → elem  (h x) ( ≈-to-≡ eq x )
ek=h : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ {_} {a} {b} {f} {g} e )  o k h eq ] ≈ h ]
ek=h {_} {_} {_} {_} {_} {d} {h} {eq} = refl 

open sequ

--           equalizer-c = sequ a b f g
--          ; equalizer = λ e → equ e

SetsIsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g
SetsIsEqualizer {c₂} a b f g = record { 
               fe=ge  = fe=ge { c₂ } {a} {b} {f} {g}
             ; k = λ {d} h eq → k { c₂ } {a} {b} {f} {g} {d} h eq
             ; ek=h = λ {d} {h} {eq} → ek=h {c₂} {a} {b} {f} {g} {d} {h} {eq}
             ; uniqueness  = uniqueness
       } where
           injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
           injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
           lemma5 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ {_} {a} {b} {f} {g} (k h fh=gh x) ≡ equ (k' x)
           lemma5 refl  x  = refl   -- somehow this is not equal to ≈-to-≡
           uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets  ( λ ( x : d ) →  begin
                k h fh=gh x
             ≡⟨ elm-cong ( k h fh=gh x) (  k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x )  ⟩
                k' x
             ∎  ) where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning


open Functor

----
-- C is locally small i.e. Hom C i j is a set c₁
--
record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
   field
     hom→ : {i j : Obj C } →    Hom C i j →  I → I 
     hom← : {i j : Obj C } →  ( f : I → I  ) →  Hom C i j 
     hom-iso : {i j : Obj C } →  { f : Hom C i j } →   hom← ( hom→ f )  ≡ f 
     -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y

open Small 

ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
   (i : Obj C ) →　 Set c₁
ΓObj s  Γ i = FObj Γ i

ΓMap :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
    {i j : Obj C } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f ) 

slid :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) → (x : Obj C)  →   I → I
slid C I s x = hom→ s ( id1 C x )

record slim  { c₂ }  { I OC :  Set  c₂ } 
                ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I ) → sobj i → sobj j ) 
      :  Set   c₂  where
   field 
       slproj : ( i : OC ) → sobj i 
       slequ : (i j : OC) (f :  I → I  ) → sequ OC (sobj j) (λ x →  smap f (slproj i) ) (λ x → slproj j )
   slprod : sproduct OC  sobj
   slprod = record { proj = slproj }
   slmap  :  { i j :  OC  }  → (f : I → I ) → sobj i → sobj j
   slmap f x = smap f x
open slim

open import HomReasoning
open NTrans


Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
    → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) ))  Γ
Cone {c₁} C I s  Γ =  record {
               TMap = λ i →  λ se → proj ( slprod se ) i
             ; isNTrans = record { commute = commute1 }
      } where
        commute1 :   {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod se) a) ] ≈
             Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
        commute1  {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
                  FMap Γ f (proj  (slprod se ) a )
             ≡⟨  ≡cong ( λ g → FMap Γ g (proj  (slprod se) a))  (sym ( hom-iso s  ) ) ⟩
                  FMap Γ  (hom← s ( hom→ s f))  (proj  (slprod se) a)
             ≡⟨  fe=ge0 (slequ se a b ( hom→ s f) ) ⟩
                  proj (slprod se) b
             ∎  ) where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning

SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
    → Limit Sets C Γ
SetsLimit { c₂} C I s Γ = record { 
           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
         ; t0 = Cone C I s Γ 
         ; isLimit = record {
               limit  = limit1
             ; t0f=t = λ {a t i } → refl
             ; limit-uniqueness  =  λ {a t f }  → limit-uniqueness {a} {t} {f}
          }
       }  where
          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
          limit1 a t = λ x →  record {
               slequ =  λ i j f → elem {!!} ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ))
               ; slproj =  λ i → ( TMap t i ) x
             }
          limit-uniqueness :  {a : Obj Sets} {t :  NTrans C Sets (K Sets C a) Γ}  {f : Hom Sets a (slim  (ΓObj s Γ) (ΓMap s Γ))} → ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ)  i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
          limit-uniqueness {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
                  limit1 a t x
             ≡⟨ {!!} ⟩
                  f x
             ∎  ) where
                  open  import  Relation.Binary.PropositionalEquality
                  open ≡-Reasoning