# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511885593 -32400
# Node ID e8d29695741ea59f055db6fcddce973f3e996a5a
# Parent  2439a142aba2f05bdccb4b10f8039581d144dc97
...

diff -r 2439a142aba2 -r e8d29695741e monad→monoidal.agda
--- a/monad→monoidal.agda	Tue Nov 28 10:47:05 2017 +0900
+++ b/monad→monoidal.agda	Wed Nov 29 01:13:13 2017 +0900
@@ -14,6 +14,7 @@
 open import monoidal 
 open import Category.Sets 
 
+import Relation.Binary.PropositionalEquality
 
 Monad→HaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → HaskellMonoidalFunctor ( Monad.T m )
 Monad→HaskellMonoidalFunctor monad = record {
@@ -29,7 +30,7 @@
 
 Monad→IsHaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → IsHaskellMonoidalFunctor (  Monad.T m )
      ( HaskellMonoidalFunctor.unit ( Monad→HaskellMonoidalFunctor m ) ) ( HaskellMonoidalFunctor.φ ( Monad→HaskellMonoidalFunctor m ) )
-Monad→IsHaskellMonoidalFunctor monad = record {
+Monad→IsHaskellMonoidalFunctor {l} monad = record {
           natφ = natφ 
         ; assocφ = assocφ  
         ; idrφ =  idrφ  
@@ -39,10 +40,50 @@
           unit = HaskellMonoidalFunctor.unit ( Monad→HaskellMonoidalFunctor monad ) 
           φ =  HaskellMonoidalFunctor.φ ( Monad→HaskellMonoidalFunctor monad )
           isM = Monoidal.isMonoidal MonoidalSets 
+          μ = NTrans.TMap (Monad.μ monad) 
           open IsMonoidal
+          id : { a : Obj (Sets {l}) } → a → a
+          id x = x
           natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
              → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
-          natφ = {!!}
+          natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin
+                  FMap F (map f g) (φ (x , y))
+             ≡⟨⟩ 
+                  FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (μ (Σ a (λ k → b))  (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) x))
+             ≡⟨⟩ 
+                  (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ・ (μ (Σ a (λ k → b))))  (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) x)
+             ≡⟨ ≡-cong ( λ h → h  (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) x)  ) (IsNTrans.commute (NTrans.isNTrans  (Monad.μ monad) ))   ⟩ 
+               ( μ  (Σ c (λ v → d)) ・ (( FMap F ( FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)))) ・ (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)))) x
+             ≡⟨  sym (≡-cong ( λ h →   ( μ  (Σ c (λ v → d)) ・  h ) x )   (IsFunctor.distr (Functor.isFunctor F )) )  ⟩ 
+                  (μ (Σ c (λ v → d)) ・ FMap F (( FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ・ (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) ))) x
+             ≡⟨⟩ 
+                  μ (Σ c (λ v → d)) (FMap F (λ x₁ → FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y)) x)
+             ≡⟨⟩ 
+                  (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y)))) x
+             ≡⟨ {!!} ⟩ 
+                  (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → FMap F ((λ xy → f (proj₁ xy) , g (proj₂ xy)) ・  (λ g₁ → x₁ , g₁) ) y))) x
+             ≡⟨⟩ 
+                 μ  (Σ c (λ v → d)) (FMap F (λ x₁ → FMap F (λ x₂ → f x₁ , g x₂) y) x)
+             ≡⟨⟩ 
+               ( μ  (Σ c (λ v → d)) ・ (FMap F (λ x₁ → FMap F (λ k → f x₁ , g k) y))) x
+             ≡⟨⟩ 
+                μ  (Σ c (λ x₁ → d)) (FMap F (λ x₁ → FMap F (λ k → f x₁ , g k) y) x)
+             ≡⟨⟩ 
+                μ  (Σ c (λ x₁ → d)) (FMap F ((λ f₁ → FMap F (λ k → f₁ , g k) y) ・ f) x)
+             ≡⟨ {!!} ⟩ 
+                μ  (Σ c (λ x₁ → d)) (((FMap F (λ f₁ → FMap F (λ k → f₁ , g k) y)) ・ (FMap F f)) x)
+             ≡⟨⟩ 
+                μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ k → f₁ , g k) y) (FMap F f x))
+             ≡⟨⟩ 
+                  μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ k → ((λ g₁ → f₁ , g₁) (g k))) y) (FMap F f x))
+             ≡⟨ {!!}  ⟩ 
+                  μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) (FMap F f x))
+             ≡⟨⟩
+                  φ (FMap F f x , FMap F g y)
+             ∎ 
+             where
+                  open Relation.Binary.PropositionalEquality
+                  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φ = {!!}
@@ -66,7 +107,7 @@
 
 Monad→IsApplicative : {l : Level } (m : Monad (Sets {l} ) ) → IsApplicative (  Monad.T m ) 
           ( Applicative.pure (  Monad→Applicative m )  ) ( Applicative.<*> (  Monad→Applicative m ) )
-Monad→IsApplicative monad = record {
+Monad→IsApplicative {l} monad = record {
           identity = identity 
        ;  composition = composition 
        ;  homomorphism  = homomorphism 
@@ -75,11 +116,31 @@
           F = Monad.T monad
           pure = Applicative.pure (  Monad→Applicative monad ) 
           _<*>_ = Applicative.<*> (  Monad→Applicative monad ) 
+          isM = Monoidal.isMonoidal ( MonoidalSets {l} )
+          η = NTrans.TMap (Monad.η monad ) 
+          μ = NTrans.TMap (Monad.μ monad) 
+          open IsMonoidal
+          id : { a : Obj (Sets {l}) } → a → a
+          id x = x
+          left : {n : Level} { a b : Set n} → { x y : a → b } { h : a }  → ( x ≡ y ) → x h ≡ y h
+          left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
           identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
-          identity = {!!}
+          identity {a} {u} = {!!}
           composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
               → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
-          composition = {!!}
+          composition {a} {b} {c} {u} {v} {w} = begin
+                 (( pure _・_ <*> u ) <*> v ) <*> w
+             ≡⟨⟩ 
+                μ  c (FMap F (λ k → FMap F k w) (μ  (a → c) (FMap F (λ k → FMap F k v) (μ ((a → b) → a → c)
+                    (FMap F (λ k → FMap F k u) (η ((b → c) → (a → b) → a → c) (λ f g x → f (g x))))))))
+             ≡⟨ {!!} ⟩ 
+                μ  c (FMap F (λ k → FMap F k (μ b (FMap F (λ k₁ → FMap F k₁ w) v))) u)
+             ≡⟨⟩ 
+                 u  <*> (v  <*> w)
+             ∎ 
+             where
+                  open Relation.Binary.PropositionalEquality
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
           homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
           homomorphism = {!!}
           interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u