Mercurial > hg > Members > kono > Proof > category
changeset 750:b45587696acf
assoc start
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Dec 2017 17:55:28 +0900 |
| parents | 274f6a03e11c |
| children | 7fd8c4fbafb9 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 34 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sun Dec 10 15:16:24 2017 +0900 +++ b/monad→monoidal.agda Sun Dec 10 17:55:28 2017 +0900 @@ -89,9 +89,26 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning 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φ = {!!} + assocφ {x} {y} {z} {a} {b} {c} = monoidal.≡-cong ( λ h → h a ) ( begin + ( λ a → φ (a , φ (b , c)) ) + ≈⟨⟩ + ( λ a → μ ( x * ( y * z ) ) (FMap F (λ f → FMap F (λ g → f , g) (μ (y * z ) (FMap F (λ f₁ → FMap F (λ g → f₁ , g) c) b))) a)) + ≈⟨⟩ + μ ( x * ( y * z ) ) o (FMap F (λ f → FMap F (λ g → f , g) (μ (y * z ) (FMap F (λ f₁ → FMap F (λ g → f₁ , g) c) b)))) + ≈⟨ {!!} ⟩ + FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o + (μ ( ( x * y ) * z ) o (FMap F (λ f → FMap (Monad.T monad) (λ g → f , g) c) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) )))) + ≈⟨⟩ + ( λ a → FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) + (μ ( ( x * y ) * z ) (FMap F (λ f → FMap (Monad.T monad) (λ g → f , g) c) (μ (x * y ) (FMap F (λ f → FMap F (λ g → f , g) b) a))))) + ≈⟨⟩ + ( λ a → FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) ) + ∎ ) where + open ≈-Reasoning Sets hiding ( _o_ ) proj1 : {a : Obj Sets} → _*_ {l} {l} a One → a proj1 = proj₁ + proj2 : {a : Obj Sets} → _*_ {l} {l} One a → a + proj2 = 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)) ) @@ -127,7 +144,7 @@ ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} idL ⟩ FMap F proj₁ o FMap F ( λ f → ( f , OneObj )) ≈↑⟨ distr F ⟩ - FMap F ( ( λ ( x : _*_ {l} {l} a One ) → proj₁ x ) o ( λ f → ( f , OneObj ))) + FMap F (proj1 o ( λ f → ( f , OneObj ))) ≈⟨⟩ FMap F (id1 Sets a ) ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩ @@ -139,7 +156,21 @@ ( λ x → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ) ≈⟨⟩ ( λ x → FMap F proj₂ (μ (One * a ) (FMap F (λ f → FMap F (λ g → f , g) x) (η One OneObj)))) - ≈⟨ {!!} ⟩ + ≈⟨⟩ + ( λ x → ( FMap F proj₂ o (μ (One * a ) o (FMap F (λ f → FMap F (λ g → f , g) x) o η One) )) OneObj ) + ≈⟨ monoidal.≡-cong ( λ h → λ x → ( FMap F proj₂ o (μ (One * a ) o h x )) OneObj ) ( extensionality (Sets {l}) ( λ x → nat (Monad.η monad ) )) ⟩ + (λ x → (FMap F proj2 o (μ (One * a) o (η (FObj F (One * a)) o FMap (identityFunctor {_} {_} {_} {Sets {l}} ) (λ f → FMap F (λ g → f , g) x) ))) OneObj) + ≈⟨⟩ + FMap F proj2 o (μ (One * a ) o (η (FObj F (One * a)) o ( FMap F (λ g → (OneObj , g )) ))) + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj2} ( assoc {_} {_} {_} {_} {μ (One * a )} {η (FObj F (One * a))} { FMap F (λ g → (OneObj , g )) } ) ⟩ + FMap F proj₂ o (( μ (One * a ) o η (FObj F (One * a))) o FMap F (λ g → (OneObj , g )) ) + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj2} ( car {_} {_} {_} {_} {_} { FMap F (λ g → (OneObj , g ))} ( IsMonad.unity1 (Monad.isMonad monad )) ) ⟩ + FMap F proj₂ o (id1 Sets (FObj F (One * a)) o FMap F (λ g → (OneObj , g )) ) + ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj2} ( idL ) ⟩ + FMap F proj₂ o FMap F (λ g → (OneObj , g ) ) + ≈↑⟨ distr F ⟩ + FMap F ( proj2 o (λ g → (OneObj , g ) )) + ≈⟨⟩ FMap F (id1 Sets a ) ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩ id1 Sets (FObj F a)