Mercurial > hg > Members > kono > Proof > category

changeset 1122:47694f2bcd7f

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 Sun, 07 Jul 2024 13:54:12 +0900
parents 7df508f857cc
children b6ab443f7a43
files src/monad→monoidal.agda
diffstat 1 files changed, 2 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/monad→monoidal.agda	Sun Jul 07 13:50:25 2024 +0900
+++ b/src/monad→monoidal.agda	Sun Jul 07 13:54:12 2024 +0900
@@ -100,7 +100,8 @@
                TMap μ (x * y * z) (TMap μ (FObj T (x * y * z)) (FMap T (λ f → FMap T (λ g → FMap T (λ h → f , g , h) c) b) a))  
                    ≡⟨ cong ( λ k → TMap μ (x * (y * z)) (TMap μ _ k) ) (begin
                      FMap T (λ f → FMap T (λ g → FMap T (λ h → f , g , h) c) b) a  ≡⟨ fcong a (λ w → fdistr b) ⟩ 
-                     FMap T (λ z₁ → FMap T _ (FMap T _ b)) a  ≡⟨ fcong a (λ w → (fcong _ (λ z → fdistr c)) ) ⟩ 
+                     FMap T (λ z₁ → FMap T (λ z₂ → FMap T (λ z₃ → Iso.≅→ (mα-iso isM) (z₂ , z₃)) c) (FMap T (λ g → z₁ , g) b)) a
+                          ≡⟨ fcong a (λ w → (fcong _ (λ z → fdistr c)) ) ⟩ 
                      FMap T (λ z₁ → FMap T (λ x₁ → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ g → x₁ , g) c)) (FMap T (λ g → z₁ , g) b)) a  ∎ ) ⟩
                TMap μ (x * y * z) (TMap μ (FObj T (x * y * z)) (FMap T (λ z₁ → FMap T (λ x₁ → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ g → x₁ , g) c)) (FMap T (λ g → z₁ , g) b)) a))
                    ≡⟨ cong ( λ k → TMap μ (x * (y * z)) (TMap μ _ k) ) (fdistr a) ⟩