Mercurial > hg > Members > kono > Proof > category
changeset 763:37ddc8228832
monad to applicative done.
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 23:43:41 +0900 |
| parents | 96afaa736186 |
| children | 01c618d94278 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 14 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 23:08:25 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 23:43:41 2017 +0900 @@ -418,27 +418,31 @@ ( λ x → μ b (FMap F (λ k → FMap F k (η a x)) u)) ≈⟨⟩ ( λ x → (μ b o (FMap F (λ k → (FMap F k o η a) x))) u ) - ≈⟨ {!!} ⟩ - ( λ x → (μ b o (FMap F (λ k → (η b o k ) x))) u ) - ≈⟨ {!!} ⟩ + ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) (fcong F ( extensionality Sets ( λ k → ≡cong ( λ h → h x ) ( nat ( Monad.η monad )))))) ⟩ + ( λ x → (μ b o FMap F (λ k → (η b o k ) x)) u ) + ≈⟨⟩ + (λ x → (μ b o FMap F ( η b o (λ f → f x) )) u) + ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( fcong F (nat ( Monad.η monad ) ))) ⟩ + (λ x → (μ b o FMap F ( FMap F (λ f → f x) o η (a → b) )) u) + ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( distr F ) ) ⟩ ( λ x → (μ b o ( FMap F ( FMap F (λ f → f x) ) o FMap F ( η (a → b) ))) u ) - ≈⟨ {!!} ⟩ + ≈⟨⟩ ( λ x → ( (μ b o (FMap F ( FMap F (λ f → f x) )) ) o FMap F ( η (a → b) )) u ) - ≈⟨ {!!} ⟩ + ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( h o FMap F ( η (a → b) )) u ) ( nat ( Monad.μ monad ))) ⟩ ( λ x → ((FMap F (λ f → f x) o (μ (a → b) o FMap F ( η (a → b) )))) u ) - ≈⟨ {!!} ⟩ + ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → (FMap F (λ f → f x) o h ) u ) ( IsMonad.unity2 ( Monad.isMonad monad ) )) ⟩ ( λ x → ((FMap F (λ f → f x) o id1 Sets (FObj F (a → b)))) u ) - ≈⟨ {!!} ⟩ + ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → h u ) ( idR {_} {_} {FMap F (λ f → f x)} )) ⟩ ( λ x → ( FMap F (λ f → f x) ) u ) - ≈⟨ {!!} ⟩ + ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → h u ) ( idL {_} {_} { FMap F (λ f → f x) }) ) ⟩ ( λ x → (id1 Sets (FObj F b ) o FMap F (λ f → f x) ) u ) - ≈⟨ {!!} ⟩ + ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → (h o FMap F (λ f → f x) ) u ) ( IsMonad.unity1 ( Monad.isMonad monad ) )) ⟩ ( λ x → (( μ b o η (FObj F b )) o FMap F (λ f → f x) ) u ) ≈⟨⟩ ( λ x → ( μ b o ( η (FObj F b ) o FMap F (λ f → f x))) u ) ≈⟨⟩ ( λ x → ( μ b o ( η (FObj F b ) o (λ k → FMap F k u) )) (λ f → f x) ) - ≈⟨ {!!} ⟩ + ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h ) (λ f → f x) ) ( nat ( Monad.η monad ))) ⟩ ( λ x → ( μ b o ((FMap F (λ k → FMap F k u) ) o η ((f : a → b) → b))) (λ f → f x) ) ≈⟨⟩ ( λ x → (( μ b o (FMap F (λ k → FMap F k u) )) o η ((f : a → b) → b)) (λ f → f x) )