Mercurial > hg > Members > kono > Proof > category
changeset 756:03f09d7dfffd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 11:45:04 +0900 |
| parents | a1c3d82be8c8 |
| children | a4074765abf8 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 23 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 11:01:23 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 11:45:04 2017 +0900 @@ -319,8 +319,30 @@ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( μ ((a → b) → a → c) o (FMap F (λ k → FMap F k u) o η ((b → c) → (a → b) → a → c)) ) ) ) ) ) (λ f g x → f (g x)) ) + ≈⟨ {!!} ⟩ -- nat η + ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( + μ ((a → b) → a → c) o (η (FObj F ((a → b) → a → c)) o (λ k → FMap F k u) ) + ) ) ) ) ) (λ f g x → f (g x)) ) + ≈⟨ {!!} ⟩ -- assoc + ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( + ( μ ((a → b) → a → c) o η (FObj F ((a → b) → a → c)) ) o (λ k → FMap F k 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 ( + id1 Sets (FObj (Monad.T monad) ((a → b) → a → c)) o (λ k → FMap F k u) + ) ) ) ) ) (λ f g x → f (g x)) ) + ≈⟨ {!!} ⟩ -- idR + ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( + λ k → FMap F k u + ) ) ) ) ) (λ f g x → f (g x)) ) + ≈⟨⟩ + ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( λ j → ( FMap F (λ k → FMap F k v) o FMap F j ) u )))) (λ f g x → f (g x)) ) ≈⟨ {!!} ⟩ - ( λ w → (μ c o (FMap F ( λ k → ( FMap F k o ( μ b o FMap F (λ h → FMap F h w))) v )) ) u ) + ( λ 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 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) ) ≈⟨⟩