# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1493002115 -32400
# Node ID 9e727ce08b2c6efe12aa8380c9b260b37852fdd5
# Parent  ecef5008cc174a6df08f6d5d9756c7b47e5c7758
on going ...

diff -r ecef5008cc17 -r 9e727ce08b2c SetsCompleteness.agda
--- a/SetsCompleteness.agda	Mon Apr 24 11:04:14 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 24 11:48:35 2017 +0900
@@ -247,8 +247,8 @@
                 } 
               uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ) )} →
                     ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) →  (f' : I → I ) →  (x : a ) 
-                     → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f' x )  ≡ snequ1 (f x ) f'
-              uniquness2 cif=t f' x = {!!}
+                     →  equ (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t f' x)) ≡ equ (snequ1 (f x) f')
+              uniquness2 cif=t f' x = refl 
               uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (Γ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 ]
               uniquness1 {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
@@ -260,7 +260,7 @@
                            extensionality Sets  ( λ  j  →
                                extensionality Sets  ( λ  f'  →
                                    extensionality Sets  ( λ  x  → 
-                  elm-cong (  elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f' x )) (snequ1 (f x) f' ) ? )
+                  elm-cong (  elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f' x )) (snequ1 (f x) f' ) (uniquness2 cif=t f' x ) )
                            )))
                      ) ⟩
                    record { snequ1 = λ {i} {j} f' → snequ1 (f x ) f' }