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

diff -r b9c086bda3cc -r f19dab948e39 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Sun Mar 19 13:28:12 2017 +0900
+++ b/SetsCompleteness.agda	Mon Mar 20 12:50:21 2017 +0900
@@ -120,21 +120,24 @@
            k {d} h eq = λ x → elem  (h x) ( cong ( λ y → y x ) eq )
            ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
            ek=h {d} {h} {eq} = refl 
-           uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {eq : 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 ] → Sets [ k h eq  ≈ k' ]
-           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets ( λ x →  
+           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
+           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 x
-              ≡⟨ {!!} ⟩
-                 elem  (h x) ( ≡-cong ( λ y → y x ) fh=gh  )
-              ≡⟨ {!!} ⟩
-                 elem  (equ (k' x)) {!!}
-              ≡⟨ {!!} ⟩
-                 k' x
+                 k h fh=gh y
+              ≡⟨⟩
+                  elem  (h y) (fhy=ghy d h y fh=gh )
+              ≡⟨ ? ⟩
+                 k' y
               ∎  
-             ) where
+              where
                   open  import  Relation.Binary.PropositionalEquality 
                   open ≡-Reasoning 
+           uniqueness :   {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 ] → Sets [ k h fh=gh  ≈ k' ]
+           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets ( λ y →  repl {d} {h} {fh=gh}{k'}  y ek'=h   ) 
 
 
 open Functor