--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/monoidal.agda	Mon Nov 20 22:52:55 2017 +0900
@@ -0,0 +1,84 @@
+open import Level
+open import Level
+open import Level
+open import Category
+module 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
+
+record _≅_ {ℓ : Level } ( C B : Set ℓ ) : Set  (suc ℓ )  where
+   field
+         ≅→ : C → B
+         ≅← : B → C
+         ≅Id→  :  {x : C} →  ≅← ( ≅→ x  ) ≡  x
+         ≅Id←  :  {x : B} →  ≅→ ( ≅← x  ) ≡  x
+
+infix  4 _≅_
+
+record IsMonoidal  {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 
+
+--      -- 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 )    ] ]
+
+record Monoidal  {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 : IsMonoidal C m-i m-bi
+
+
+open import Category.Cat
+
+record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
+        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
+  field
+     a : {!!}
+
+record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
+        : 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
+  field
+      MF : Functor C D
+  F● : (a b : Obj C ) → Functor ( C × C ) D
+  F● a b =  record {
+       FObj = λ x  → (FObj MF a) ●  (FObj MF b)
+     ; FMap = λ {a} {b} f → FMap (Monoidal.m-bi N) (  FMap MF  ? , FMap MF {!!} )
+     ; isFunctor = record {
+     }
+    }
+  F⊗ : (a b : Obj C ) → Functor ( C × C ) D
+  F⊗ a b =  record {
+       FObj = λ x → FObj MF ( a ⊗ b )
+     ; FMap = λ {a} {b} f →  FMap MF ( FMap (Monoidal.m-bi M) (  {!!}  , {!!} ) )
+     ; isFunctor = record {
+     }
+    }
+  field
+      φab : {a b : Obj C} → NTrans  ( C × C ) D  (F● a b) (F⊗ a b )
+      φ   : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
+      isMonodailFunctor : IsMonoidalFunctor  M N