# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1615100269 -32400
# Node ID 98f4120584884a316af25d48f7db94c3f46e5c6d
# Parent  d9419216ae0ca84c5b357b6efad57251a5d38fd8
...

diff -r d9419216ae0c -r 98f412058488 src/SetsCompleteness.agda
--- a/src/SetsCompleteness.agda	Sun Mar 07 15:51:45 2021 +0900
+++ b/src/SetsCompleteness.agda	Sun Mar 07 15:57:49 2021 +0900
@@ -219,15 +219,11 @@
           ee : Hom Sets (sequ a b f g)  a
           ee (elem y eq) = y
           k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d
-          k {d} h hf=hg ec = {!!} where
+          k {d} h hf=hg = cd where
+             ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a  -- (λ x → h (f x)) ≡ (λ x → h (g x))
+             ca eq = {!!}
              cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d
-             cd ec = h ( f {!!} ) 
-             ff : sequ a b f g → sequ a d ( Sets [ h o f ]) (Sets [ h o g ])  
-             ff (elem x eq) = elem x (cong (λ k → k x ) hf=hg )
-             gg : {y : a} → f y ≡ g y → sequ a d ( Sets [ h o f ]) (Sets [ h o g ])  
-             gg {y} eq  = ff (ec eq)
-             hoge : ({y : a} → f y ≡ g y → sequ a d ( Sets [ h o f ]) (Sets [ h o g ]) ) → d
-             hoge ed = {!!}
+             cd = {!!}
           ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] }
            →   Sets [ Sets [ k h eq o equc f g ] ≈ h ]
           ke=h {d} {h} {eq} =  extensionality Sets  ( λ  x → begin