Mercurial > hg > Members > kono > Proof > category

changeset 1030:76a7d5a8a4e0

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 Tue, 30 Mar 2021 17:58:55 +0900
parents 348b5c6d5670
children 52c98490c877
files src/CCCSets.agda
diffstat 1 files changed, 25 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Tue Mar 30 16:03:44 2021 +0900
+++ b/src/CCCSets.agda	Tue Mar 30 17:58:55 2021 +0900
@@ -161,35 +161,47 @@
         ... | case1 t = true
         ... | case2 f = false
 
-        b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  (mono : Mono Sets m ) → (x : b) → image m (m x)
-        b2i m mono x = isImage x
-        i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  (mono : Mono Sets m ) → {y : a} → image m y → b
-        i2b m mono (isImage x) = x
-        b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  (mono : Mono Sets m ) → (x : b) → i2b m mono (b2i m mono x) ≡ x
-        b2i-iso m mono x = refl
+        image-iso : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m )  (y : a) → (i0 i1 : image m y ) → i0 ≡ i1
+        image-iso = {!!}
+        tchar¬Img : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  (y : a) → tchar m mono y ≡ false → ¬ image m y
+        tchar¬Img  m mono y eq im with lem (image m y) 
+        ... | case2 n  = n im
+        b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → image m (m x)
+        b2i m x = isImage x
+        i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  {y : a} → image m y → b
+        i2b m (isImage x) = x
+        b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  (x : b) → i2b m (b2i m x) ≡ x
+        b2i-iso m x = refl
         b2s : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) →  sequ a Bool (tchar m mono)  (λ _ → true )
         b2s m mono x with tchar m mono (m x) | inspect (tchar m mono) (m x)
         ... | true | record {eq = eq1} = elem (m x) eq1
-        ... | false | record { eq = eq1 } = {!!}
+        ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
+        ... | t = ⊥-elim (t (isImage x)) 
         s2i  : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono)  (λ _ → true )) → image m (equ e)
         s2i {a} {b} m mono (elem y eq) with lem (image m y)
         ... | case1 im = im
-
-
+        s2ii : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → (eq1 : tchar m mono (m x)  ≡ true)
+            → s2i m mono (elem (m x ) eq1) ≡ isImage x
+        s2ii m mono x eq1 with lem (image m (m x))
+        ... | case1 im = s2ii0 where
+            s2ii0 :  im ≡ isImage x
+            s2ii0 = image-iso m mono (m x) im (isImage x)
         isol : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → IsoL Sets m (λ (e : sequ a Bool (tchar m mono)  (λ _ → true )) → equ e )
         isol {a} {b} m mono  = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ;
                iso→  =  extensionality Sets ( λ x → iso1 x )
              ; iso←  =  extensionality Sets ( λ x → iso2 x) } ; iso≈L = {!!} } where
           b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
-          b→s x = {!!}
+          b→s x = b2s m mono x
           b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
-          b←s (elem y eq) = {!!}
+          b←s (elem y eq) = i2b m (s2i m mono (elem y eq))
           iso1 : (x : b) → b←s ( b→s x ) ≡  x
           iso1 x with  tchar m mono (m x) | inspect (tchar m mono ) (m x)
           ... | true | record { eq = eq1 }  = begin
-             b←s ( elem (m x) eq1 )  ≡⟨ {!!} ⟩
+             b←s ( elem (m x) eq1 )  ≡⟨⟩
+             i2b m (s2i m mono (elem (m x ) eq1 ))  ≡⟨ cong (λ k → i2b m k) (s2ii m mono x eq1 ) ⟩
+             i2b m (isImage x)  ≡⟨⟩
              x ∎ where open ≡-Reasoning
-          iso1 x | false | record { eq = eq1 } = {!!}
+          iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x))
           iso2 : (x : sequ a Bool (tchar m mono) (λ _ → true) ) →  (Sets [ b→s o b←s ]) x ≡ id1 Sets (sequ a Bool (tchar m mono) (λ _ → true)) x
           iso2 (elem y eq) = {!!}
         imequ   : {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 ])