Mercurial > hg > Members > kono > Proof > category

changeset 1027:5ae0290c34b4

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:57:12 +0900
parents 7916bde5e57b
children 28569574e3cf
files src/CCCSets.agda
diffstat 1 files changed, 3 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Mon Mar 29 21:25:32 2021 +0900
+++ b/src/CCCSets.agda	Mon Mar 29 21:57:12 2021 +0900
@@ -193,18 +193,13 @@
           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 )
-          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 eq1 with tcharImg m mono y eq1
-          ... | t1 = {!!}
-          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)) 
+          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 = ?
           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 )  ≡⟨ {!!}  ⟩
+             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)   ≡⟨⟩