Mercurial > hg > Members > kono > Proof > category
changeset 761:e7c673eba848
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 22:03:32 +0900 |
| parents | d17c556b9343 |
| children | 96afaa736186 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 42 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 20:37:22 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 22:03:32 2017 +0900 @@ -390,8 +390,20 @@ ( λ x → pure f <*> pure x ) ≈⟨⟩ ( λ x → μ b (FMap F (λ k → FMap F k (η a x)) ((η (a → b) f)) )) - ≈⟨ {!!} ⟩ - η b o f + ≈⟨⟩ + μ b o ( λ x → (FMap F ( λ k → FMap F k (η a x) ) o η (a → b) ) f ) + ≈⟨ cdr {_} {_} {_} {_} {_} {μ b} ( extensionality Sets ( λ x → ≡cong ( λ h → h f ) ( nat ( Monad.η monad ) ))) ⟩ + μ b o ( λ x → (η (FObj F b) o (λ k → FMap F k (η a x)) ) f ) + ≈⟨⟩ + μ b o (η (FObj F b) o (FMap F f o η a )) + ≈⟨⟩ + (μ b o η (FObj F b)) o (FMap F f o η a ) + ≈⟨ car ( IsMonad.unity1 ( Monad.isMonad monad )) ⟩ + id1 Sets (FObj F b ) o (FMap F f o η a ) + ≈⟨ idL ⟩ + FMap F f o η a + ≈⟨ nat ( Monad.η monad ) ⟩ + η b o f ≈⟨⟩ ( λ x → η b (f x) ) ≈⟨⟩ @@ -404,7 +416,35 @@ ( λ x → u <*> pure x ) ≈⟨⟩ ( λ 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 ) + ≈⟨ {!!} ⟩ + ( λ x → (μ b o ( η (FObj F b) o FMap F ( {!!} ))) u ) + ≈⟨ {!!} ⟩ + ( λ x → (μ b o ((FMap F (FMap F (λ f → f x) )) o η (FObj F (a → b) ))) u ) + ≈⟨ {!!} ⟩ + ( λ x → (((FMap F (λ f → f x) o μ (a → b)) o η (FObj F (a → b)))) u ) + ≈⟨⟩ + ( λ x → ((FMap F (λ f → f x) o (μ (a → b) o η (FObj F (a → b))))) u ) + ≈⟨ {!!} ⟩ + ( λ x → ((FMap F (λ f → f x) o id1 Sets (FObj F (a → b)))) u ) + ≈⟨ {!!} ⟩ + ( λ x → ( FMap F (λ f → f x) ) u ) + ≈⟨ {!!} ⟩ + ( λ x → (id1 Sets (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 FMap F (λ f → f x))) u ) + ≈⟨⟩ + ( λ x → ( μ b o ( η (FObj F b ) o (λ k → FMap F k u) )) (λ f → f x) ) + ≈⟨ {!!} ⟩ + ( λ 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) ) + ≈⟨⟩ ( λ x → μ b (FMap F (λ k → FMap F k u) (η ((f : a → b) → b) (λ f → f x))) ) ≈⟨⟩ ( λ x → pure (λ f → f x) <*> u )