# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490069932 -32400
# Node ID 221dd46ded354019d219df8b09b10dc9c33380e0
# Parent  1fca61019bdfe673dcf41be98537ef5e82e2285d
on going ...

diff -r 1fca61019bdf -r 221dd46ded35 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Tue Mar 21 10:14:04 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 21 13:18:52 2017 +0900
@@ -124,6 +124,8 @@
            fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh
            fuga :  (x : a  ) → { fx=gx :  f x ≡ g x  } →  sequ a b  f g 
            fuga  x { fx=gx } = elem  x fx=gx
+           hoge : sequ a b f g →   sequ a b f g
+           hoge ( elem x eq ) =   elem  x eq
            repl :   {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)} → ( y : d ) →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → k h fh=gh y ≡ k' y
            repl {d} {h} {fh=gh} {k'} y ek'=h = 
@@ -133,11 +135,17 @@
                  elem  (h y) (fhy=ghy d h y fh=gh )
               ≡⟨⟩
                  fuga  (h y ) {fhy=ghy d h y fh=gh }
-              ≡⟨ sym ( Category.cong (λ f → fuga (f y )   ) ek'=h )  ⟩
-                 fuga ( ( λ e → equ e ) ( k' y ) ) {?}
+              ≡⟨ sym ( Category.cong (λ f → fuga (f y )  ) ek'=h )  ⟩
+                 fuga ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)}
               ≡⟨⟩
                  ( λ e → fuga ( equ e )) ( k' y ) 
+              ≡⟨⟩
+                 ( λ e → elem  (equ e) (fe=ge0 e )) ( k' y ) 
               ≡⟨ {!!} ⟩
+                  hoge ( k' y ) 
+              ≡⟨ {!!} ⟩
+                 ( λ e → e ) ( k' y ) 
+              ≡⟨⟩
                  k' y
               ∎  
               where