# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512377740 -32400
# Node ID 15ded3383319d629fa25ad9cb69851cd82b50390
# Parent  a4792945cd9ba714cb6ab74a1e85adb1030d64cd
add monad to monoidal

diff -r a4792945cd9b -r 15ded3383319 monad→monoidal.agda
--- a/monad→monoidal.agda	Mon Dec 04 12:36:43 2017 +0900
+++ b/monad→monoidal.agda	Mon Dec 04 17:55:40 2017 +0900
@@ -10,10 +10,35 @@
 open import Relation.Binary
 
 open Functor
+open NTrans
 
 open import monoidal 
 open import Category.Sets 
 
+Monad→MonoidalFunctor : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) ( m : Monad C ) ( monoidal : Monoidal C )
+     → MonoidalFunctor monoidal monoidal    -- should be monoidal to kleisli-monoidal
+Monad→MonoidalFunctor C M Mono = record {
+      MF = Monad.T M
+    ; ψ  = NTrans.TMap (Monad.η M )  ( Monoidal.m-i Mono )
+    ; isMonodailFunctor = record {
+             φab  = record { TMap = φab 
+               ;  isNTrans = record { commute = {!!}
+               } } 
+         ;   associativity  = {!!}
+         ;   unitarity-idr = {!!}
+         ;   unitarity-idl = {!!}
+      }
+  } where
+     T = Monad.T M
+     μ = TMap ( Monad.μ M )
+     η = TMap ( Monad.η M )
+     _⊗_ : (x y : Obj C ) → Obj C
+     _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal Mono) ) x y
+     _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
+     _□_ f g = FMap (Monoidal.m-bi Mono) ( f , g )
+     φab  : (a : Obj (C × C)) → Hom C (FObj (Functor● C C Mono (Monad.T M)) a) (FObj (Functor⊗ C C Mono (Monad.T M)) a)
+     φab (x , y ) = C [ μ (x ⊗ y) o {!!}   ]
+
 import Relation.Binary.PropositionalEquality
 
 Monad→HaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → HaskellMonoidalFunctor ( Monad.T m )