Mercurial > hg > Members > kono > Proof > category
diff src/CCCSets.agda @ 1027:5ae0290c34b4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Mar 2021 21:57:12 +0900 |
| parents | 7916bde5e57b |
| children | 28569574e3cf |
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) ≡⟨⟩