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