--- a/monoidal.agda	Tue Nov 21 00:11:10 2017 +0900
+++ b/monoidal.agda	Tue Nov 21 09:57:42 2017 +0900
@@ -13,33 +13,59 @@
 
 open Functor
 
-record _≅_ {ℓ : Level } ( C B : Set ℓ ) : Set  (suc ℓ )  where
+record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
+         (x y : Obj C )
+        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
    field
-         ≅→ : C → B
-         ≅← : B → C
-         ≅Id→  :  {x : C} →  ≅← ( ≅→ x  ) ≡  x
-         ≅Id←  :  {x : B} →  ≅→ ( ≅← x  ) ≡  x
+         ≅→ :  Hom C x y 
+         ≅← :  Hom C y x 
+         iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
+         iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]
 
-infix  4 _≅_
-
-record IsMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
+record IsStrictMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
   infixr 9 _⊗_
   _⊗_ : ( x y : Obj C ) → Obj C
   _⊗_ x y = FObj BI ( x , y )
   field
       mα : {a b c : Obj C} →  ( a ⊗ b) ⊗ c  ≡  a ⊗ ( b ⊗ c )
-      mλa : (a : Obj C) → I ⊗ a  ≡ a 
-      mσa : (a : Obj C) → a ⊗ I  ≡ a 
+      mλ : (a : Obj C) → I ⊗ a  ≡ a 
+      mσ : (a : Obj C) → a ⊗ I  ≡ a 
+
+record StrictMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
+        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
+  field
+      m-i : Obj C
+      m-bi : Functor ( C × C ) C 
+      isMonoidal : IsStrictMonoidal C m-i m-bi
+
 
---      -- non strict version includes 6 naturalities
---      mα→ : {a b c : Obj C} → Hom C ( ( a ⊗ b) ⊗ c)  ( a ⊗ ( b ⊗ c ) )
---      mα← : {a b c : Obj C} → Hom C ( a ⊗ ( b ⊗ c )) ( ( a ⊗ b) ⊗ c)
---      mα-iso→ : {a b c : Obj C} →  C [ C [ mα←  o  mα→ ] ≈ id1 C (( a ⊗  b)  ⊗ c )  ] 
---      mα-iso← : {a b c : Obj C} →  C [ C [ mα→  o  mα← ] ≈ id1 C (  a ⊗ (b   ⊗ c )) ] 
---      mα→nat1 : {a a' b c : Obj C} →  ( f : Hom C a a' ) →
---         C [ C [ FMap BI ( f , id1 C (FObj BI ( b , c )  ))  o mα→ {a} ]  ≈
---            C [   mα→ {a'}  o FMap BI ( FMap BI (f , id1 C b ) , id1 C c )    ] ]
+--      non strict version includes 5 naturalities
+record IsMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
+        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
+  open Iso 
+  infixr 9 _⊗_
+  _⊗_ : ( x y : Obj C ) → Obj C
+  _⊗_ x y = FObj BI ( x , y )
+  field
+      mα-iso : {a b c : Obj C} →  Iso C ( ( a ⊗ b) ⊗ c)  ( a ⊗ ( b ⊗ c ) ) 
+      mλ-iso : {a : Obj C} →  Iso C ( I ⊗ a)  a 
+      mσ-iso : {a : Obj C} →  Iso C ( a ⊗ I)  a 
+      mα→nat1 : {a a' b c : Obj C} →  ( f : Hom C a a' ) →
+         C [ C [ FMap BI ( f , id1 C ( b ⊗ c ))  o ≅→ (mα-iso {a} {b} {c}) ]  ≈
+            C [   ≅→ (mα-iso )  o FMap BI ( FMap BI (f , id1 C b ) , id1 C c )    ] ]
+      mα→nat2 : {a b b' c : Obj C} →  ( f : Hom C b b' ) →
+         C [ C [ FMap BI ( id1 C a , FMap BI ( f , id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
+            C [   ≅→ (mα-iso )  o FMap BI ( FMap BI (id1 C a , f )  , id1 C c ) ] ]
+      mα→nat3 : {a b c c' : Obj C} →  ( f : Hom C c c' ) →
+         C [ C [ FMap BI ( id1 C a , FMap BI ( id1 C b , f ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
+            C [   ≅→ (mα-iso )  o FMap BI ( id1 C ( a ⊗ b ) , f ) ] ]
+      mλ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
+         C [ C [ f o ≅→ (mλ-iso {a} ) ]  ≈
+            C [   ≅→ (mλ-iso )  o FMap BI ( id1 C I  , f )    ] ]
+      mσ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
+         C [ C [ f o ≅→ (mσ-iso {a} ) ]  ≈
+            C [   ≅→ (mσ-iso )  o FMap BI ( f , id1 C I  )    ] ]
 
 record Monoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
@@ -51,10 +77,25 @@
 
 open import Category.Cat
 
+
 record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
+      ( MF :   Functor C D )
+      ( F● :   Functor ( C × C ) D )
+      ( F⊗ :   Functor ( C × C ) D )
+      ( φab :  NTrans  ( C × C ) D  F● F⊗ )
+      ( φ   :  Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) ) )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
+  _⊗_ : (x y : Obj C ) → Obj C
+  _⊗_ x y =  (IsMonoidal._⊗_ (Monoidal.isMonoidal M) ) x y
+  _●_ : (x y : Obj D ) → Obj D
+  _●_ x y =  (IsMonoidal._⊗_ (Monoidal.isMonoidal N) ) x y
+  open Iso
+  open Monoidal
+  open IsMonoidal hiding ( _⊗_ )
+  αD :  {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
+  αD {a} {b} {c} =  ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) 
   field
-     a : {!!}
+     comm1 :  {!!}
 
 record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
         : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
@@ -81,4 +122,4 @@
   field
       φab :  NTrans  ( C × C ) D  F● F⊗ 
       φ   : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
-      isMonodailFunctor : IsMonoidalFunctor  M N
+      isMonodailFunctor : IsMonoidalFunctor  M N MF F● F⊗ φab φ