Mercurial > hg > Members > kono > Proof > category
changeset 746:2d1fb7adcafe
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 Dec 2017 11:51:30 +0900 |
| parents | 9dbbbb295a09 |
| children | 37bffde965b3 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 9 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Fri Dec 08 18:36:31 2017 +0900 +++ b/monad→monoidal.agda Sat Dec 09 11:51:30 2017 +0900 @@ -104,23 +104,21 @@ ≈⟨ {!!} ⟩ ( λ x → ( FMap F proj₁ o ( μ (a * One ) o (FMap F {!!} o η One ) )) OneObj ) ≈⟨ {!!} ⟩ - ( λ x → ( FMap F proj₁ o ( μ (a * One ) o ( η (FObj F (a * One ) ) o FMap F {!!} ) )) x ) - ≈⟨ {!!} ⟩ - ( λ x → ( FMap F proj₁ o ( μ ( a * One ) o ( FMap F {!!} o η (FObj F a )))) x ) + ( λ x → ( FMap F proj₁ o ( μ (a * One ) o ( η (FObj F (a * One ) ) o FMap F (λ f → ( f , OneObj ) )) )) x ) ≈⟨ {!!} ⟩ - FMap F proj₁ o ( μ ( a * One ) o ( η (FObj F (a * One )) o FMap F ( λ g → ( g , OneObj ) ))) - ≈↑⟨ cdr ( cdr ( nat ( Monad.η monad ))) ⟩ - FMap F proj₁ o ( μ ( a * One ) o ( FMap F ( FMap F (λ g → ( g , OneObj ))) o η (FObj F a ))) + FMap F proj₁ o ( μ (a * One ) o ( η (FObj F (a * One ) ) o FMap F ((λ g → (λ f → ( f , g ) )) OneObj ) ) ) ≈⟨⟩ - FMap F proj₁ o (( μ ( a * One ) o FMap F (FMap F (λ g → ( g , OneObj ) ) )) o η (FObj F a )) + 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 (λ g → ( g , OneObj )) o μ a ) o η (FObj F a )) + FMap F proj₁ o (( FMap F (λ f → ( f , OneObj )) o μ a ) o η (FObj F a )) ≈⟨ cdr assoc ⟩ - FMap F proj₁ o ( FMap F (λ g → ( g , OneObj )) o ( μ a o η (FObj F a ))) + 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 (λ g → ( g , OneObj )) o id1 Sets (FObj F a ) ) + 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 , λ g → ( g , OneObj ) ) + FMap F proj₁ o FMap F (λ z → z , λ f → ( f , OneObj ) ) ≈↑⟨ distr F ⟩ FMap F (id1 Sets a ) ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩