# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490565325 -32400
# Node ID d6739779b4acf86dd9c757dc4291dcb8ffb0bb5d
# Parent  4b097a010fd90ae5eb51a74014d4415d2dde13c0
on going ..

diff -r 4b097a010fd9 -r d6739779b4ac SetsCompleteness.agda
--- a/SetsCompleteness.agda	Sun Mar 26 23:17:44 2017 +0900
+++ b/SetsCompleteness.agda	Mon Mar 27 06:55:25 2017 +0900
@@ -16,7 +16,9 @@
 
 ≡cong = Relation.Binary.PropositionalEquality.cong 
 
-
+lemma1 :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
+   Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
+lemma1 refl  x  = refl
 
 record Σ {a} (A : Set a) (B : Set a) : Set a where
   constructor _,_
@@ -127,9 +129,6 @@
            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} →
-                Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
-           lemma1 refl  x  = refl
            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 (k h fh=gh x) ≡ equ (k' x)
            lemma5 refl  x  = refl   -- somehow this is not equal to lemma1
@@ -179,8 +178,10 @@
              ; limit-uniqueness  = {!!}
            }
        }  where
-          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets {!!}) i) (iproduct (Obj Sets) (λ I → ΓObj (Obj Sets)))
-          e = {!!}
+          eqa : {i j : Obj Sets} (f : Hom Sets i j) → sequ (Obj Sets) (Obj Sets) {!!} {!!}         --  {!!} {!!} (FMap Γ f o  proj i) ( proj j ) 
+          eqa f = {!!}
+          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets ( sequ {!!} {!!} {!!} {!!}  )) i ) (iproduct (Obj Sets) (λ I → ΓObj (Obj Sets)))
+          e i =  λ x → record { pi1  = λ i → record { obj =  sequ ? {!!} {!!} {!!}    } }
           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 → {!!} ) ] ≈