Mercurial > hg > Members > kono > Proof > category
changeset 748:a83145326258
yellow on idrφ
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Dec 2017 14:30:11 +0900 |
| parents | 37bffde965b3 |
| children | 274f6a03e11c |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 32 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sun Dec 10 11:28:03 2017 +0900 +++ b/monad→monoidal.agda Sun Dec 10 14:30:11 2017 +0900 @@ -99,21 +99,34 @@ FMap F proj₁ o (μ (a * One ) o FMap F (λ f → ( FMap F (λ g → f , g) ((η One) OneObj)))) ≈⟨⟩ FMap F proj₁ o (μ (a * One ) o FMap F (λ f → ( FMap F (λ g → f , g) o η One ) OneObj )) - ≈⟨ {!!} ⟩ - FMap F proj₁ o ( μ (a * One ) o ( η (FObj F (a * One ) ) o FMap F ((λ g → (λ f → ( f , g ) )) OneObj ) ) ) + ≈⟨ cdr ( cdr ( fcong F ( begin + (λ f → ( FMap F (λ g → f , g) o η One ) OneObj ) + ≈⟨ monoidal.≡-cong ( λ h → λ f → (h f) OneObj ) (extensionality Sets (λ f → ( + begin + FMap F (λ g → f , g) o η One + ≈⟨ nat ( Monad.η monad ) ⟩ + η ( a * One) o FMap identityFunctor (λ g → f , g) + ≈⟨⟩ + η (a * One) o ( λ g → ( f , g ) ) + ∎ + ))) ⟩ + (λ f → ( η (a * One) o ( λ g → ( f , g ) ) ) OneObj ) + ≈⟨⟩ + η (a * One ) o ( λ f → ( f , OneObj ) ) + ∎ + ))) ⟩ + FMap F proj₁ o (μ (a * One ) o FMap F ( η (a * One ) o ( λ f → ( f , OneObj )))) + ≈⟨ cdr ( cdr ( distr F )) ⟩ + FMap F proj₁ o (μ (a * One ) o ( FMap F ( η (a * One )) o FMap F ( λ f → ( f , OneObj )))) + ≈⟨ cdr assoc ⟩ + FMap F proj₁ o ( ( μ (a * One ) o FMap F ( η (a * One ))) o FMap F ( λ f → ( f , OneObj ))) + ≈⟨ cdr ( car ( IsMonad.unity2 (Monad.isMonad monad ))) ⟩ + FMap F proj₁ o ( id1 Sets (FObj F (a * One)) o FMap F ( λ f → ( f , OneObj ))) + ≈⟨ cdr idL ⟩ + FMap F proj₁ o FMap F ( λ f → ( f , OneObj )) + ≈↑⟨ distr F ⟩ + FMap F ( proj₁ o ( λ f → ( f , OneObj ))) ≈⟨⟩ - FMap F proj₁ o ( μ (a * One ) o ( η (FObj F (a * One ) ) o FMap F (λ f → ( f , OneObj ) ) ) ) - ≈⟨ cdr ( cdr ( nat( Monad.η monad ) )) ⟩ - FMap F proj₁ o (( μ ( a * One ) o FMap F (FMap F (λ f → ( f , OneObj ) ) )) o η (FObj F a )) - ≈⟨ cdr ( car (nat ( Monad.μ monad ))) ⟩ - FMap F proj₁ o (( FMap F (λ f → ( f , OneObj )) o μ a ) o η (FObj F a )) - ≈⟨ cdr assoc ⟩ - FMap F proj₁ o ( FMap F (λ f → ( f , OneObj )) o ( μ a o η (FObj F a ))) - ≈⟨ cdr ( cdr ( IsMonad.unity2 (Monad.isMonad monad ))) ⟩ - FMap F proj₁ o ( FMap F (λ f → ( f , OneObj )) o id1 Sets (FObj F a ) ) - ≈⟨ cdr idR ⟩ - FMap F proj₁ o FMap F (λ z → z , λ f → ( f , OneObj ) ) - ≈↑⟨ distr F ⟩ FMap F (id1 Sets a ) ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩ id1 Sets (FObj F a) @@ -198,19 +211,21 @@ ( λ w → u <*> (v <*> w) ) ∎ ) where - open ≈-Reasoning Sets + open ≈-Reasoning Sets hiding ( _o_ ) homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) homomorphism {a} {b} {f} {x} = ≡cong ( λ h → h x ) ( begin ( λ x → pure f <*> pure x ) ≈⟨⟩ ( λ x → μ b (FMap F (λ k → FMap F k (η a x)) ((η (a → b) f)) )) ≈⟨ {!!} ⟩ + η b o f + ≈⟨⟩ ( λ x → η b (f x) ) ≈⟨⟩ ( λ x → pure (f x )) ∎ ) where - open ≈-Reasoning Sets + open ≈-Reasoning Sets hiding ( _o_ ) interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u interchange {a} {b} {u} {x} = ≡cong ( λ h → h x ) ( begin ( λ x → u <*> pure x ) @@ -222,6 +237,6 @@ ( λ x → pure (λ f → f x) <*> u ) ∎ ) where - open ≈-Reasoning Sets + open ≈-Reasoning Sets hiding ( _o_ )