# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490056737 -32400
# Node ID e73c3e73a87bd53141fd3b677baf666d84f7e1e0
# Parent  f19dab948e39ebaf115b7e55236db51bfa764222
on going ...

diff -r f19dab948e39 -r e73c3e73a87b SetsCompleteness.agda
--- a/SetsCompleteness.agda	Mon Mar 20 12:50:21 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 21 09:38:57 2017 +0900
@@ -122,14 +122,22 @@
            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
+           fuga : {d : Obj Sets} { y : d } { k' : Hom Sets d (sequ a b f g)}  →  Hom Sets a {!!}
+           fuga = {!!}
            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 = 
               begin
                  k h fh=gh y
               ≡⟨⟩
-                  elem  (h y) (fhy=ghy d h y fh=gh )
-              ≡⟨ ? ⟩
+                 elem  (h y) (fhy=ghy d h y fh=gh )
+              ≡⟨ {!!} ⟩
+                 fuga (h y )
+              ≡⟨ sym ( Category.cong (λ f → fuga (f y ) ) ek'=h )  ⟩
+                 fuga ( ( λ e → equ e ) ( k' y ) )
+              ≡⟨⟩
+                 ( λ e → fuga ( equ e )) ( k' y ) 
+              ≡⟨ {!!} ⟩
                  k' y
               ∎  
               where