--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/monad→monoidal.agda	Tue Nov 28 10:47:05 2017 +0900
@@ -0,0 +1,87 @@
+open import Level
+open import Category
+module monad→monoidal where
+
+open import Data.Product renaming (_×_ to _*_)
+open import Category.Constructions.Product
+open import HomReasoning
+open import cat-utility
+open import Relation.Binary.Core
+open import Relation.Binary
+
+open Functor
+
+open import monoidal 
+open import Category.Sets 
+
+
+Monad→HaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → HaskellMonoidalFunctor ( Monad.T m )
+Monad→HaskellMonoidalFunctor monad = record {
+         unit = unit
+       ; φ = φ
+   } where
+      F = Monad.T monad
+      η = NTrans.TMap (Monad.η monad ) 
+      unit  : FObj F One
+      unit  = η One OneObj 
+      φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
+      φ {a} {b} (x , y)  =  ( NTrans.TMap (Monad.μ monad ) (a * b) ) (FMap F ( λ f → FMap F ( λ g → ( f , g )) y ) x )
+
+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 {
+          natφ = natφ 
+        ; assocφ = assocφ  
+        ; idrφ =  idrφ  
+        ; idlφ = idlφ  
+   } where
+          F = Monad.T monad
+          unit = HaskellMonoidalFunctor.unit ( Monad→HaskellMonoidalFunctor monad ) 
+          φ =  HaskellMonoidalFunctor.φ ( Monad→HaskellMonoidalFunctor monad )
+          isM = Monoidal.isMonoidal MonoidalSets 
+          open IsMonoidal
+          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φ = {!!}
+          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φ = {!!}
+          idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
+          idrφ = {!!}
+          idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
+          idlφ = {!!}
+
+
+Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m )
+Monad→Applicative monad = record {
+         pure = pure
+       ; <*> = <*>
+   } where
+      F = Monad.T monad
+      η = NTrans.TMap (Monad.η monad ) 
+      pure  : {a : Obj Sets} → Hom Sets a ( FObj F a )
+      pure {a}  = η a
+      <*>   : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
+      <*> {a} {b} f x = ( NTrans.TMap (Monad.μ monad ) b ) ( (FMap F (λ k → FMap F k x )) f )
+
+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 {
+          identity = identity 
+       ;  composition = composition 
+       ;  homomorphism  = homomorphism 
+       ;  interchange  = interchange 
+  } where
+          F = Monad.T monad
+          pure = Applicative.pure (  Monad→Applicative monad ) 
+          _<*>_ = Applicative.<*> (  Monad→Applicative monad ) 
+          identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
+          identity = {!!}
+          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 = {!!}
+          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
+          interchange = {!!}
+

--- a/monoidal.agda	Mon Nov 27 14:42:49 2017 +0900
+++ b/monoidal.agda	Tue Nov 28 10:47:05 2017 +0900
@@ -269,6 +269,7 @@
 -- so we postulate this
 --    and we cannot indent postulate ...
 postulate FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) →  ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) →  {h f : Hom C a b } →  {g k : Hom C b c } →  C [  C  [ g o h ]  ≈  C [ k o f ]  ] →  D [ D [ FMap F g o fmap h ]  ≈  D [ fmap k o FMap F f ] ]
+
 UniquenessOfFunctor :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ')  (F : Functor C D)
   {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) )
       → ( {b : Obj C } → D [ fmap  (id1 C b) ≈  id1 D (FObj F b) ] )
@@ -978,4 +979,3 @@
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
 
---