Mercurial > hg > Members > kono > Proof > category
changeset 1121:7df508f857cc
assocφ passed
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2024 13:50:25 +0900 |
| parents | 121e28cccdf6 |
| children | 47694f2bcd7f |
| files | src/monad→monoidal.agda |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/monad→monoidal.agda Sun Jul 07 10:18:45 2024 +0900 +++ b/src/monad→monoidal.agda Sun Jul 07 13:50:25 2024 +0900 @@ -98,10 +98,10 @@ TMap μ (x * y * z) (FMap T (TMap μ (x * y * z)) (FMap T (λ f → ( FMap T (λ g → (FMap T (λ h → f , (g , h))) c)) b ) a )) ≡⟨ sym (IsMonad.assoc isMonad _ ) ⟩ 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) ) (fcong a (λ w → begin - FMap T (λ g → FMap T (λ h → w , g , h) c) b ≡⟨ fcong b (λ w → fdistr c) ⟩ - FMap T (λ g → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ h → (w , g) , h) c)) b ≡⟨ ? ⟩ - FMap T (λ x₁ → FMap T (Iso.≅→ (mα-iso isM)) (FMap T (λ g → x₁ , g) c)) (FMap T (λ g → w , g) b) ∎ ) ) ⟩ + ≡⟨ 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 (λ 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) ⟩ TMap μ (x * y * z) (TMap μ (FObj T (x * y * z))