--- a/SetsCompleteness.agda	Sun Mar 26 19:41:44 2017 +0900
+++ b/SetsCompleteness.agda	Sun Mar 26 23:17:44 2017 +0900
@@ -121,10 +121,10 @@
            k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
            ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
            ek=h {d} {h} {eq} = refl 
-           fhy=ghy : {d : Obj Sets } { h : Hom Sets d a } {y : d } →  (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ])  → f (h y) ≡ g (h y)
-           fhy=ghy {d} {h} {y} fh=gh = ≡cong ( λ f → f y ) fh=gh
            irr : {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
            irr refl refl = refl
+           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
            elm-cong :   (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' )
            lemma1 :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
@@ -164,28 +164,25 @@
        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
+open IProduct
 
--- 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} = {!!}
+SetsLimit :  { c₂ : Level}  →  Limit Sets Sets Γ
+SetsLimit { c₂}  = record { 
+           a0 =  {!!}
+         ; t0 = record { 
+               TMap = λ i → Sets  [ proj i o  e i ]
+             ; isNTrans = record { commute = {!!} } 
+           }
+         ; isLimit = record {
+               limit  = {!!}
+             ; t0f=t = {!!}
+             ; limit-uniqueness  = {!!}
+           }
+       }  where
+          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets {!!}) i) (iproduct (Obj Sets) (λ I → ΓObj (Obj Sets)))
+          e = {!!}
+          proj :  (i : Obj Sets) → ( prod : iproduct (Obj Sets) (λ i → ΓObj (Obj Sets) )) → FObj Γ i
+          proj i prod =  record { obj = {!!} }
+          comm1 :  {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → {!!} ) ] ≈
+                       Sets [ (λ lim → {!!}) o FMap (K Sets Sets {!!}) f ] ]
+          comm1 {a} {b} {f} = {!!}