--- a/monoidal.agda	Wed Nov 22 14:07:17 2017 +0900
+++ b/monoidal.agda	Thu Nov 23 09:34:15 2017 +0900
@@ -1,5 +1,3 @@
-open import Level
-open import Level
 open import Level
 open import Category
 module monoidal where
@@ -291,7 +289,7 @@
   field
       MF    : Functor C D
       unit  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
-      **    : {a b : Obj C} → Hom D ((FObj MF a) ●  (FObj MF b )) ( FObj MF ( a ⊗ b ) )
+      φ    : {a b : Obj C} → Hom D ((FObj MF a) ●  (FObj MF b )) ( FObj MF ( a ⊗ b ) )
 
 open import Category.Sets
 
@@ -302,18 +300,58 @@
 data One {c : Level} : Set c where
   OneObj : One   -- () in Haskell ( or any one object set )
 
-isoSets  :{c₁ : Level} {a : Obj (Sets {c₁} ) } → Iso (Sets {c₁}) a ( a * One {c₁} )
-isoSets {a} = record {
-         ≅→ =  λ x → ( x , OneObj ) ;
-         ≅← =  λ x →   proj₁ x ;
-         iso→  =  refl ;
-         iso←  =  iso←
+SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} )  (Sets {c})
+SetsTensorProduct =   record {
+       FObj = λ x  →  proj₁ x  *  proj₂ x
+     ; FMap = λ {x : Obj ( Sets × Sets ) } {y} f → map (proj₁ f)  (proj₂ f)
+     ; isFunctor = record {
+             ≈-cong   = ≈-cong 
+             ; identity = refl
+             ; distr    = refl
      }
-  where
-    lemma : {a : Obj Sets } → (x : a * One) → (Sets [ (λ x₁ → x₁ , OneObj) o proj₁ ]) x ≡ id1 Sets (a * One) x
-    lemma (_ , OneObj ) = refl
-    iso← : {a : Obj Sets} → Sets [ Sets [ (λ x → x , OneObj) o proj₁ ] ≈ id1 Sets (a * One) ]
-    iso← {a} = extensionality Sets ( λ x → lemma x ) 
+    } where
+        ≈-cong : {a b : Obj (Sets × Sets)} {f g : Hom (Sets × Sets) a b} →
+                (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ]
+        ≈-cong (refl , refl) =  refl
+
+
+
+MonoidalSets : {c : Level} → Monoidal (Sets {c})
+MonoidalSets = record {
+      m-i = One ;
+      m-bi = SetsTensorProduct  ;
+      isMonoidal = record {
+              mα-iso  =  record { ≅→  =  mα→ ; ≅← =  mα← ; iso→  = refl ; iso← = refl } ;
+              mλ-iso  =  record { ≅→  =  mλ→ ; ≅← =  mλ← ; iso→  = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ;
+              mρ-iso  =  record { ≅→  =  mρ→ ; ≅← =  mρ← ; iso→  = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ;
+              mα→nat1  = λ f → refl  ;
+              mα→nat2  =  λ f → refl  ;
+              mα→nat3  =  λ f → refl  ;
+              mλ→nat  =  λ f → refl  ;
+              mρ→nat  =  λ f → refl  ;
+              comm-penta  = refl ;
+              comm-unit  = refl
+      }
+   } where
+       _⊗_ : ( a b : Obj Sets ) → Obj Sets
+       _⊗_ a b = FObj SetsTensorProduct (a , b )
+       mα→ : {a b c : Obj Sets} →  Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
+       mα→ ((a , b) , c ) =  (a , ( b , c ) )
+       mα← : {a b c : Obj Sets} →  Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c )
+       mα← (a , ( b , c ) ) =  ((a , b) , c )
+       mλ→ : {a  : Obj Sets} →  Hom Sets ( One ⊗ a ) a
+       mλ→ (_ , a) =  a
+       mλ← : {a  : Obj Sets} →  Hom Sets  a ( One ⊗ a )
+       mλ←  a = ( OneObj , a )
+       mλiso : {a : Obj Sets} (x : One ⊗ a) →  (Sets [ mλ← o mλ→ ]) x ≡ id1 Sets (One ⊗ a) x
+       mλiso (OneObj , _ ) = refl
+       mρ→ : {a  : Obj Sets} →  Hom Sets ( a ⊗ One )  a
+       mρ→ (a , _) =  a
+       mρ← : {a  : Obj Sets} →  Hom Sets a ( a ⊗ One ) 
+       mρ←  a = ( a , OneObj )
+       mρiso : {a : Obj Sets} (x : a ⊗ One ) →  (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
+       mρiso (_ , OneObj ) = refl
+
 
 
 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
@@ -324,7 +362,8 @@
   **    : {a b : Obj Sets} → FObj f a →  FObj f b →  FObj f ( a * b ) 
   ** x y  = φ ( x , y )
 
---  HaskellMonoidalFunctor f → MonoidalFunctor
+lemma0 :  {c : Level} ( f : Functor (Sets {c}) (Sets {c}) ) → HaskellMonoidalFunctor f → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
+lemma0 f = {!!}
 
 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where
@@ -348,5 +387,5 @@
      open HaskellMonoidalFunctor
      pure  :  {a : Obj Sets} → Hom Sets a ( FObj f a )
      pure {a} x = FMap f ( λ y → x ) (unit mono)
-     <*> :   {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
-     <*> {a} {b} x y = FMap f ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  ( ** mono  x y  )
+     <*> :   {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b        --  ** mono  x y 
+     <*> {a} {b} x y = FMap f ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  (φ mono ( x , y ))