Mercurial > hg > Members > kono > Proof > category
changeset 757:a4074765abf8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 15:58:52 +0900 |
| parents | 03f09d7dfffd |
| children | 74d197dd8a68 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 18 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 11:45:04 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 15:58:52 2017 +0900 @@ -341,7 +341,25 @@ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( λ j → ( FMap F (( λ k → FMap F k v) o j ) u ))))) (λ f g x → f (g x)) ) ≈⟨⟩ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) + ≈⟨⟩ + ( λ w → ( μ c o ((FMap F (λ k → FMap F k w) o μ (a → c) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )))) u ) + ≈⟨ {!!} ⟩ -- nat μ + ( λ w → ( μ c o ((μ (FObj F c) o FMap F (FMap F (λ k → FMap F k w) ) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )))) u ) + ≈⟨⟩ -- assoc + ( λ w → ( μ c o (μ (FObj F c) o ( FMap F (FMap F (λ k → FMap F k w) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) ))))) u ) ≈⟨ {!!} ⟩ + ( λ w → ( μ c o (μ (FObj F c) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) ))))) u ) + ≈⟨⟩ + ( λ w → (( μ c o μ (FObj F c) ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )) u ) + ≈⟨ {!!} ⟩ + ( λ w → (( μ c o (FMap F ( μ c )) ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )) u ) + ≈⟨⟩ + ( λ w → ( μ c o (FMap F ( μ c ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) + ≈⟨ {!!} ⟩ + ( λ w → ( μ c o (FMap F ( μ c o (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) + ≈⟨ {!!} ⟩ + ( λ w → ( μ c o (FMap F ( (λ x → ( μ c o (FMap F (λ k → FMap F k w) o (FMap F (λ g x₁ → x (g x₁)) ) )) v )))) u ) + ≈⟨ {!!} ⟩ ( λ w → ( μ c o (FMap F (λ k → ( FMap F k o ( μ b o FMap F (λ h → FMap F h w))) v )) ) u ) ≈⟨⟩ ( λ w → μ c (FMap F (λ k → FMap F k (μ b (FMap F (λ h → FMap F h w) v))) u) )