Mercurial > hg > Members > kono > Proof > category

changeset 1026:7916bde5e57b

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 Mon, 29 Mar 2021 21:25:32 +0900
parents 49fbc57ea772
children 5ae0290c34b4
files src/CCCSets.agda
diffstat 1 files changed, 16 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Mon Mar 29 19:55:41 2021 +0900
+++ b/src/CCCSets.agda	Mon Mar 29 21:25:32 2021 +0900
@@ -168,6 +168,8 @@
         ... | case2 n  = n im
         img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b
         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₁)
@@ -181,7 +183,7 @@
         img-x-cong0 m mono y s t = img-x-cong m mono y y refl s t
         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→  =  Mono.isMono mono (Sets [ b←s o b→s ]) (id1 Sets _) ( extensionality Sets ( λ x → iso1 x ))
+               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 with tchar m mono (m x) | inspect (tchar m mono ) (m x)
@@ -192,16 +194,21 @@
           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 )
           bs=x : (x : b) → (y : a) → y ≡ m x → (eq : tchar m mono y ≡ true ) →  b←s (elem y eq) ≡ x
-          bs=x x y refl t with tcharImg m mono y t
+          bs=x x y refl eq1 with tcharImg m mono y eq1
           ... | t1 = {!!}
-          iso1 : (x : b) → ( Sets [ m o (Sets Category.o b←s) b→s ] ) x ≡  ( Sets [ m o Category.Category.Id Sets ] ) x
+          b←s0 : (x : b) → sequ a Bool (tchar m mono) (λ _ → true) → image m (m x)
+          b←s0 x (elem x₁ eq) with lem (image m (m x))
+          ... | case1 t = t
+          ... | case2 n = ⊥-elim ( n (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 }  = begin
-             m ( b←s ( elem (m x) eq1 ))  ≡⟨⟩
-             m (img-x m  (isImage (b←s ( elem (m x) eq1 )) )) ≡⟨ {!!} ⟩
-             m (img-x m  (tcharImg m mono (m x) eq1 ) ) ≡⟨ {!!} ⟩
-             m (img-x m  (isImage x) ) ≡⟨⟩
-             m x ∎ where open ≡-Reasoning
+          ... | 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 )  ≡⟨ {!!}  ⟩
+             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)   ≡⟨⟩
+             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
           iso2 (elem y eq) = {!!}