--- a/monoidal.agda	Wed Nov 22 04:12:14 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 04:42:48 2017 +0900
@@ -112,39 +112,42 @@
     } where
   _●_ : (x y : Obj D ) → Obj D
   _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
+  _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d )
+  _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
+  F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b )
+  F f = FMap MF f
   ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
-        D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f))
-        ≈ FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) ]
+        D [  (F (proj₁ f) ■ F (proj₂ f)) ≈  (F (proj₁ g) ■ F (proj₂ g)) ]
   ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning D in begin
-       FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f))
+        F (proj₁ f) ■ F (proj₂ f)
      ≈⟨ fcong (Monoidal.m-bi N) (  fcong MF (  proj₁ f≈g ) , fcong MF ( proj₂ f≈g ))  ⟩
-       FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g))
+        F (proj₁ g) ■ F (proj₂ g)
      ∎ 
-  identity : {a : Obj (C × C)} → D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ (id1 (C × C) a)) , FMap MF (proj₂ (id1 (C × C) a)))
+  identity : {a : Obj (C × C)} → D [  (F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a)))
         ≈ id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) ]
   identity {a} =   let open ≈-Reasoning D in begin
-        FMap (Monoidal.m-bi N) (FMap MF (proj₁ (id1 (C × C) a)) , FMap MF (proj₂ (id1 (C × C) a)))
+         F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a))
      ≈⟨ fcong  (Monoidal.m-bi N) (  IsFunctor.identity (isFunctor MF )  ,  IsFunctor.identity (isFunctor MF ))  ⟩
-        FMap (Monoidal.m-bi N) ( id1 D (FObj MF (proj₁ a)) , id1 D (FObj MF (proj₂ a)))
+         id1 D (FObj MF (proj₁ a)) ■ id1 D (FObj MF (proj₂ a))
      ≈⟨ IsFunctor.identity (isFunctor  (Monoidal.m-bi N)) ⟩
         id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a))
      ∎
   distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} →
-     D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ ((C × C) [ g o f ])) , FMap MF (proj₂ ((C × C) [ g o f ])))
-       ≈ D [ FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) o FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f)) ] ]
+     D [  (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ])))
+       ≈ D [  (F (proj₁ g) ■ F (proj₂ g)) o  (F (proj₁ f) ■ F (proj₂ f)) ] ]
   distr {a} {b} {c} {f} {g} =  let open ≈-Reasoning D in begin
-       FMap (Monoidal.m-bi N) (FMap MF (proj₁ ((C × C) [ g o f ])) , FMap MF (proj₂ ((C × C) [ g o f ])))
+        (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ])))
      ≈⟨ fcong (Monoidal.m-bi N) (  IsFunctor.distr ( isFunctor  MF) ,  IsFunctor.distr ( isFunctor MF )) ⟩
-        FMap (Monoidal.m-bi N) ( D [  FMap MF (proj₁ g)  o FMap MF (proj₁ f) ]  , D [ FMap MF (proj₂ g) o FMap MF (proj₂ f) ] )
+         ( F (proj₁ g)  o F (proj₁ f) ) ■ (  F (proj₂ g) o F (proj₂ f)  )
      ≈⟨ IsFunctor.distr ( isFunctor  (Monoidal.m-bi N)) ⟩
-       FMap (Monoidal.m-bi N) (FMap MF (proj₁ g) , FMap MF (proj₂ g)) o FMap (Monoidal.m-bi N) (FMap MF (proj₁ f) , FMap MF (proj₂ f))
+        (F (proj₁ g) ■ F (proj₂ g)) o  (F (proj₁ f) ■ F (proj₂ f))
      ∎
 
 Functor⊗ :  {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( M : Monoidal C ) 
       ( MF :   Functor C D ) →  Functor ( C × C ) D
 Functor⊗ C D M MF =  record {
        FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
-     ; FMap = λ {a} {b} f →  FMap MF ( FMap (Monoidal.m-bi M) (  proj₁ f , proj₂ f) )
+     ; FMap = λ {a} {b} f →  F ( FMap (Monoidal.m-bi M) (  proj₁ f , proj₂ f) )
      ; isFunctor = record {
              ≈-cong   = ≈-cong
              ; identity = identity
@@ -153,31 +156,35 @@
     } where
   _⊗_ : (x y : Obj C ) → Obj C
   _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
+  _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
+  _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
+  F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b )
+  F f = FMap MF f
   ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
-     D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) ≈ FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) ]
+     D [ F ( (proj₁ f □ proj₂ f)) ≈ F ( (proj₁ g □ proj₂ g)) ]
   ≈-cong {a} {b} {f} {g} f≈g = IsFunctor.≈-cong (isFunctor MF ) ( IsFunctor.≈-cong (isFunctor  (Monoidal.m-bi M) ) f≈g  )
-  identity : {a : Obj (C × C)} → D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ (id1 (C × C) a) , proj₂ (id1 (C × C) a)))
+  identity : {a : Obj (C × C)} → D [ F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a)))
       ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ]
   identity {a} = let open ≈-Reasoning D in begin
-        FMap MF (FMap (Monoidal.m-bi M) (proj₁ (id1 (C × C) a) , proj₂ (id1 (C × C) a)))
+        F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a)))
      ≈⟨⟩
-        FMap MF (FMap (Monoidal.m-bi M) (id1 (C × C) a ) )
+        F (FMap (Monoidal.m-bi M) (id1 (C × C) a ) )
      ≈⟨ fcong MF ( IsFunctor.identity (isFunctor (Monoidal.m-bi M) )) ⟩
-        FMap MF (id1 C (proj₁ a ⊗ proj₂ a))
+        F (id1 C (proj₁ a ⊗ proj₂ a))
      ≈⟨ IsFunctor.identity (isFunctor MF) ⟩
         id1 D (FObj MF (proj₁ a ⊗ proj₂ a))
      ∎
   distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → D [
-        FMap MF (FMap (Monoidal.m-bi M) (proj₁ ((C × C) [ g o f ]) , proj₂ ((C × C) [ g o f ])))
-    ≈ D [ FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) o FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) ] ]
+        F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ])))
+    ≈ D [ F ( (proj₁ g □ proj₂ g)) o F ( (proj₁ f □ proj₂ f)) ] ]
   distr {a} {b} {c} {f} {g} =  let open ≈-Reasoning D in begin
-        FMap MF (FMap (Monoidal.m-bi M) (proj₁ ((C × C) [ g o f ]) , proj₂ ((C × C) [ g o f ])))
+        F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ])))
      ≈⟨⟩
-        FMap MF (FMap (Monoidal.m-bi M) ( (C × C)  [ g o f ] ))
+        F (FMap (Monoidal.m-bi M) ( (C × C)  [ g o f ] ))
      ≈⟨ fcong MF ( IsFunctor.distr (isFunctor (Monoidal.m-bi M))) ⟩
-        FMap MF (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ])
+        F (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ])
      ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩
-        FMap MF (FMap (Monoidal.m-bi M) (proj₁ g , proj₂ g)) o FMap MF (FMap (Monoidal.m-bi M) (proj₁ f , proj₂ f)) 
+        F ( proj₁ g □ proj₂ g) o F ( proj₁ f □ proj₂ f) 
      ∎