Mercurial > hg > Members > kono > Proof > category

changeset 1028:28569574e3cf

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 15:20:08 +0900
parents 5ae0290c34b4
children 348b5c6d5670
files src/CCCSets.agda
diffstat 1 files changed, 22 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Mon Mar 29 21:57:12 2021 +0900
+++ b/src/CCCSets.agda	Tue Mar 30 15:20:08 2021 +0900
@@ -160,6 +160,21 @@
         tchar {a} {b} m mono y with lem (image m y )
         ... | case1 t = true
         ... | case2 f = false
+
+        s2i : {a b : Obj Sets} (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
+        i2s : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → {y : a} →  (i : image m y) → sequ a Bool (tchar m mono)  (λ _ → true )
+        i2s {a} {b} m mono {y} i with lem (image m y) | inspect (tchar m mono) y
+        ... | case1 (isImage x) | record { eq = eq1 } = elem (m x) eq1
+        ... | case2 n | record { eq = eq1 } = ⊥-elim (n i) 
+        open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+        ii : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → {y : a} → (i : image m y) →  s2i m mono ( i2s m mono i ) ≅  i
+        ii {a} {b} m mono {y} i with lem (image m y) | inspect (tchar m mono) y
+        ... | case2 n | t =  ⊥-elim (n i)
+        ... | case1 (isImage x) |  record { eq = eq1 }  = {!!}
+        ss : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono)  (λ _ → true )) → i2s m mono ( s2i m mono e ) ≡ e
+        ss = {!!}
         tcharImg : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → tchar m mono y ≡ true → image m y
         tcharImg  m mono y eq with lem (image m y)
         ... | case1 t = t
@@ -170,7 +185,6 @@
         img-x m {.(m x)} (isImage x) = x
         m-img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → (t : image m y ) → m (img-x m t) ≡ y
         m-img-x m (isImage x) = refl
-        open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
         img-cong : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y y' : a) → y ≡ y' → (s : image m y ) (t : image m y') → s ≅ t
         img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
             with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
@@ -193,16 +207,15 @@
           b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
           b←s (elem y eq) with tchar m mono y | inspect (tchar m mono ) y
           ... | true | record { eq = eq1 } = img-x m (tcharImg m mono y eq1 )
-          bs1 : (y : a) → (eq1 : tchar m mono y ≡ true ) →  b←s ( elem y eq1 ) ≡ img-x m (tcharImg m mono y eq1 ) 
-          bs1 y eq1 = ?
+          i←s :  Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) (image m {!!}) 
+          i←s  (elem y eq) = {!!}
+          bs1 : (y : a) → (eq1 : tchar m mono y ≡ true ) →  m (b←s ( elem y eq1 )) ≡ y
+          bs1 y eq1 with tcharImg m mono y eq1
+          ... | isImage x = {!!}
           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 } with tcharImg m mono (m x) eq1 | inspect ( tcharImg m mono (m x) ) eq1 
-          ... | t | record { eq = eq2 } = begin
-             b←s ( elem (m x) eq1 )  ≡⟨ bs1 (m x) eq1 ⟩
-             img-x m (tcharImg m mono (m x) eq1 )  ≡⟨ cong (λ k → img-x m k ) eq2  ⟩
-             img-x m t ≡⟨ img-x-cong0 m mono (m x ) t (isImage x)  ⟩
-             img-x m (isImage x)   ≡⟨⟩
+          ... | true | record { eq = eq1 }  = begin
+             b←s ( elem (m x) eq1 )  ≡⟨ cong (λ k → k ! ) (Mono.isMono mono {One} (λ _ → b←s ( elem (m x) eq1 ) ) (λ _ → x ) (cong (λ k _ → k ) (bs1 (m x) eq1 ))) ⟩
              x ∎ where open ≡-Reasoning
           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