# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511190670 -32400
# Node ID c68ba494abfd349d616377d2734bc635cd96ebc4
# Parent  10ccac3bc285879f624168988373d33d7498039e
fix

diff -r 10ccac3bc285 -r c68ba494abfd monoidal.agda
--- a/monoidal.agda	Mon Nov 20 22:52:55 2017 +0900
+++ b/monoidal.agda	Tue Nov 21 00:11:10 2017 +0900
@@ -64,21 +64,21 @@
   _●_ 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 {!!} )
+  F● :  Functor ( C × C ) D
+  F●  =  record {
+       FObj = λ x  → (FObj MF (proj₁ x) ) ●  (FObj MF (proj₂ x) )
+     ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) (  FMap MF  (proj₁  f ) , FMap MF (proj₂ f)  )
      ; 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) (  {!!}  , {!!} ) )
+  F⊗ : Functor ( C × C ) D
+  F⊗  =  record {
+       FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
+     ; FMap = λ {a} {b} f →  FMap MF ( FMap (Monoidal.m-bi M) (  proj₁ f , proj₂ f) )
      ; isFunctor = record {
      }
     }
   field
-      φab : {a b : Obj C} → NTrans  ( C × C ) D  (F● a b) (F⊗ a b )
+      φab :  NTrans  ( C × C ) D  F● F⊗ 
       φ   : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
       isMonodailFunctor : IsMonoidalFunctor  M N