Mercurial > hg > Members > kono > Proof > category
changeset 749:274f6a03e11c
yellow removed
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Dec 2017 15:16:24 +0900 |
| parents | a83145326258 |
| children | b45587696acf |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 11 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sun Dec 10 14:30:11 2017 +0900 +++ b/monad→monoidal.agda Sun Dec 10 15:16:24 2017 +0900 @@ -90,6 +90,8 @@ assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) assocφ = {!!} + proj1 : {a : Obj Sets} → _*_ {l} {l} a One → a + proj1 = proj₁ idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x idrφ {a} {x} = monoidal.≡-cong ( λ h → h x ) ( begin ( λ x → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ) @@ -99,13 +101,13 @@ 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 )) - ≈⟨ cdr ( cdr ( fcong F ( begin + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( cdr {_} {_} {_} {_} {_} {μ (a * One ) } ( 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 FMap (identityFunctor {_} {_} {_} {Sets {l}} )(λ g → f , g) ≈⟨⟩ η (a * One) o ( λ g → ( f , g ) ) ∎ @@ -116,16 +118,16 @@ ∎ ))) ⟩ 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 ))) ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( cdr {_} {_} {_} {_} {_} {μ (a * One )} ( distr F )) ⟩ + FMap F proj1 o (μ (a * One ) o ( FMap F ( η (a * One )) o FMap F ( λ f → ( f , OneObj )))) + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( assoc {_} {_} {_} {_} { μ (a * One )} { FMap F ( η (a * One ))} {FMap F ( λ f → ( f , OneObj ))} ) ⟩ + FMap F proj1 o ( ( μ (a * One ) o FMap F ( η (a * One ))) o FMap F ( λ f → ( f , OneObj ))) + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( car ( IsMonad.unity2 (Monad.isMonad monad ))) ⟩ FMap F proj₁ o ( id1 Sets (FObj F (a * One)) o FMap F ( λ f → ( f , OneObj ))) - ≈⟨ cdr idL ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} idL ⟩ FMap F proj₁ o FMap F ( λ f → ( f , OneObj )) ≈↑⟨ distr F ⟩ - FMap F ( proj₁ o ( λ f → ( f , OneObj ))) + FMap F ( ( λ ( x : _*_ {l} {l} a One ) → proj₁ x ) o ( λ f → ( f , OneObj ))) ≈⟨⟩ FMap F (id1 Sets a ) ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩