Mercurial > hg > Members > kono > Proof > category

changeset 1076:5e89bbb4cf53

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 May 2021 17:09:21 +0900
parents 10b4d04b734f
children 918319d070b0
files src/CCCSets.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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))