# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512896128 -32400
# Node ID b45587696acfffcb0f0ad534924c83848b584324
# Parent  274f6a03e11c66ff1ba1f9f68d6f1b047ab606ec
assoc start

diff -r 274f6a03e11c -r b45587696acf monad→monoidal.agda
--- 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)