# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511401666 -32400
# Node ID 2807335e3fa01c81dddf7f92c4de713a9286b15f
# Parent  975aa343a963831056a10c1e65fbdb428d238552
on going ...

diff -r 975aa343a963 -r 2807335e3fa0 monoidal.agda
--- a/monoidal.agda	Thu Nov 23 09:34:15 2017 +0900
+++ b/monoidal.agda	Thu Nov 23 10:47:46 2017 +0900
@@ -362,8 +362,45 @@
   **    : {a b : Obj Sets} → FObj f a →  FObj f b →  FObj f ( a * b ) 
   ** x y  = φ ( x , y )
 
-lemma0 :  {c : Level} ( f : Functor (Sets {c}) (Sets {c}) ) → HaskellMonoidalFunctor f → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
-lemma0 f = {!!}
+lemma0 :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → HaskellMonoidalFunctor F → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
+lemma0 F mf = record {
+      MF = F
+    ; ψ  = λ _ → HaskellMonoidalFunctor.unit mf
+    ; isMonodailFunctor = record {
+             φab  = record { TMap = λ x →  φ x ; isNTrans = record { commute = comm0 } }
+         ;   associativity  = comm1
+         ;   unitarity-idr = comm2
+         ;   unitarity-idl = comm3
+      }
+  } where
+      open Monoidal 
+      open IsMonoidal hiding ( _■_ ;  _□_ )
+      M = MonoidalSets
+      isM = Monoidal.isMonoidal MonoidalSets 
+      unit = HaskellMonoidalFunctor.unit mf
+      _⊗_ : (x y : Obj Sets ) → Obj Sets
+      _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
+      _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
+      _□_ f g = FMap (m-bi M) ( f , g )
+      φ : (x : Obj (Sets × Sets) ) → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
+      φ _ z = HaskellMonoidalFunctor.φ mf z
+      comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ a ]
+        ≈ Sets [ φ b o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
+      comm0 {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → {!!} )
+      comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ (a , (b ⊗  c))
+           o Sets [  (id1 Sets (FObj F a) □ φ (b , c)) o Iso.≅→ (mα-iso isM) ] ]
+        ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ (a ⊗ b , c) o  (φ (a , b) □ id1 Sets (FObj F c)) ] ] ]
+      comm1 {a} {b} {c} =  extensionality Sets ( λ x  → {!!} )
+      comm2 : {a b : Obj Sets} → Sets [ Sets [
+         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ (a , m-i MonoidalSets) o
+             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
+      comm2 {a} {b} =  extensionality Sets ( λ x  → {!!} )
+      comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
+        Sets [ φ (m-i MonoidalSets , b) o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ]
+        ≈ Iso.≅→ (mλ-iso isM) ]
+      comm3 {a} {b} =  extensionality Sets ( λ x  → {!!} )
+
+
 
 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where