Mercurial > hg > Members > kono > Proof > category
changeset 758:74d197dd8a68
composition connected
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 17:33:29 +0900 |
| parents | a4074765abf8 |
| children | fa6b75fa1d09 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 18 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 15:58:52 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 17:33:29 2017 +0900 @@ -351,16 +351,30 @@ ( λ 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 ) - ≈⟨ {!!} ⟩ + ≈⟨ {!!} ⟩ -- Monad assoc ( λ 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 (λ 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 → ( μ c o (FMap F ((λ x → FMap F x w) o (λ g x₁ → k (g x₁))))) v ))) u ) + ≈⟨⟩ + ( λ w → ( μ c o (FMap F (λ k → ( μ c o (FMap F ((λ x → (FMap F ( k o x ) w)))) ) 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 o (FMap F (λ k → ( μ c o (FMap F ((λ x → (FMap F k o FMap F x ) w))) ) v ))) u ) + ≈⟨⟩ + ( λ w → ( μ c o (FMap F (λ k → ( μ c o (FMap F (FMap F k o (λ h → FMap F h w))) ) v ))) u ) + ≈⟨ {!!} ⟩ + ( λ w → ( μ c o (FMap F (λ k → (( μ c o ( FMap F (FMap F k ) o FMap F (λ h → FMap F h w))) ) v ))) u ) + ≈⟨⟩ + ( λ w → ( μ c o (FMap F (λ k → ((( μ c o FMap F (FMap F k )) o FMap F (λ h → FMap F h w)) ) 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 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) ) ≈⟨⟩