# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620547761 -32400
# Node ID 5e89bbb4cf53028c482a87d901098e36fb1f98f1
# Parent  10b4d04b734f1063ca2717c2b152594ca25ac911
...

diff -r 10b4d04b734f -r 5e89bbb4cf53 src/CCCSets.agda
--- a/src/CCCSets.agda	Sun May 09 16:52:27 2021 +0900
+++ b/src/CCCSets.agda	Sun May 09 17:09:21 2021 +0900
@@ -203,7 +203,13 @@
         ... | case1 im = im
         iso-m :  {a a' b : Obj Sets} (p : Hom Sets a b) (q : Hom Sets a' b) (mp : Mono Sets p) (mq : Mono Sets q) →
             Iso Sets a a' → Sets [ tchar p mp ≈ tchar q mq ]
-        iso-m {a} {a'} {b} p q mp mq i = {!!}
+        iso-m {a} {a'} {b} p q mp mq i = extensionality Sets (λ y → iso-m1 y ) where
+           iso-m1 : (y : b) → tchar p mp y ≡ tchar q mq y
+           iso-m1 y with lem (image p y) | inspect (tchar p mp) y | lem (image q y) | inspect (tchar q mq) y
+           ... | case1 (isImage x) | t | case1 x₁ | v = {!!}
+           ... | case1 (isImage x) | t | case2 x₁ | v = {!!}
+           ... | case2 x | t | case1 (isImage x₁) | v = {!!}
+           ... | case2 x | t | case2 x₁ | v = {!!}
         ker-iso :  {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true) o CCC.○ sets a ])
         ker-iso {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m  isol (extensionality Sets ( λ x → iso4 x)) where
           b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))