--- a/monoidal.agda	Tue Nov 21 22:42:33 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 02:09:22 2017 +0900
@@ -69,21 +69,21 @@
          C [ C [ f o ≅→ (mρ-iso {a} ) ]  ≈
             C [   ≅→ (mρ-iso )  o ( f ■ id1 C I  )    ] ]
   αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d)
-  αABC□1D = {!!}
+  αABC□1D {a} {b} {c} {d} {e} = (  ≅→ mα-iso  ■ id1 C d )
   αAB□CD : {a b c d e : Obj C } → Hom C  ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d))
-  αAB□CD = {!!}
+  αAB□CD {a} {b} {c} {d} {e} =   ≅→ mα-iso
   1A□BCD : {a b c d e : Obj C } → Hom C  (a □ ((b □ c ) □ d)) (a □ (b □ ( c □ d) ))
-  1A□BCD = {!!}
+  1A□BCD {a} {b} {c} {d} {e} = ( id1 C a ■   ≅→ mα-iso )
   αABC□D : {a b c d e : Obj C } → Hom C  (a □ (b □ ( c □ d) )) ((a □ b ) □ (c □ d))
-  αABC□D = {!!}
+  αABC□D {a} {b} {c} {d} {e} =  ≅← mα-iso  
   αA□BCD : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ b ) □ (c □ d))
-  αA□BCD = {!!}
+  αA□BCD {a} {b} {c} {d} {e} =  ≅→ mα-iso  
   αAIB :  {a b  : Obj C } →  Hom C (( a □ I ) □ b ) (a □ ( I □ b ))
-  αAIB = {!!}
+  αAIB {a} {b} = ≅→ mα-iso
   1A□λB : {a b  : Obj C } →  Hom C  (a □ ( I □ b )) ( a □ b )
-  1A□λB = {!!}
+  1A□λB {a} {b} =  id1 C a ■  ≅→ mλ-iso 
   ρA□IB : {a b  : Obj C } →  Hom C  (( a □ I ) □ b ) ( a □ b )
-  ρA□IB = {!!}
+  ρA□IB {a} {b} = ≅→  mρ-iso  ■  id1 C b
 
   field
       comm-penta : {a b c d e : Obj C}
@@ -120,37 +120,39 @@
   _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
   open Iso
   open Monoidal
-  open IsMonoidal 
+  open IsMonoidal hiding ( _■_ ;  _□_ )
   αC :  {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
   αC {a} {b} {c} =  ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) 
   αD :  {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) )
   αD {a} {b} {c} =  ≅→ (mα-iso (isMonoidal N) {a} {b} {c}) 
-  1●φBC :  {a b c : Obj C} → Hom D  ( FObj MF a ● ( FObj MF b ● FObj MF c ) ) ( FObj MF a ● ( FObj MF ( b ⊗ c ) ))
-  1●φBC = {!!} 
-  φAB⊗C :  {a b c : Obj C} → Hom D  ( FObj MF a ● ( FObj MF ( b ⊗ c ) )) (FObj MF ( a  ⊗ ( b  ⊗ c )))
-  φAB⊗C = {!!}
-  φAB●1 :  {a b c : Obj C} → Hom D  ( ( FObj MF a ●  FObj MF b ) ● FObj MF c ) ( FObj MF ( a ⊗ b ) ● FObj MF c )
-  φAB●1 = {!!}
-  φA⊗BC :  {a b c : Obj C} → Hom D  ( FObj MF ( a ⊗ b ) ● FObj MF c ) (FObj MF ( (a  ⊗  b ) ⊗ c ))
-  φA⊗BC = {!!}
-  FαC : {a b c : Obj C} → Hom D (FObj MF ( (a  ⊗  b ) ⊗ c )) (FObj MF ( a  ⊗ ( b  ⊗ c )))
-  FαC = {!!}
-  1●φ : { a b : Obj C } → Hom D (FObj MF a  ● Monoidal.m-i N ) ( FObj MF a ● FObj  MF ( Monoidal.m-i M ) )
-  1●φ = {!!}
-  φAIC : { a b : Obj C } → Hom D  ( FObj MF a ● FObj  MF ( Monoidal.m-i M ) ) (FObj MF ( a  ⊗ Monoidal.m-i M ))
-  φAIC = {!!}
-  FρC : { a b : Obj C } → Hom D   (FObj MF ( a  ⊗ Monoidal.m-i M ))( FObj MF a  )
-  FρC = {!!}
-  ρD : { a b : Obj C } → Hom D (FObj MF a  ● Monoidal.m-i N ) ( FObj MF a  )
-  ρD = {!!}
-  φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● FObj MF b  ) ( FObj  MF ( Monoidal.m-i M )  ● FObj MF b  )
-  φ●1 = {!!}
-  φICB : { a b : Obj C } → Hom D  ( FObj  MF ( Monoidal.m-i M )  ● FObj MF b  ) ( FObj MF (  ( Monoidal.m-i M )  ⊗ b ) )
-  φICB = {!!}
-  FλD : { a b : Obj C } → Hom D  ( FObj MF (  ( Monoidal.m-i M )  ⊗ b ) ) (FObj MF b ) 
-  FλD = {!!}
-  λD : { a b : Obj C } → Hom D  (Monoidal.m-i N ● FObj MF b  )  (FObj MF b ) 
-  λD = {!!}
+  F : Obj C → Obj D
+  F x = FObj MF x
+  1●φBC :  {a b c : Obj C} → Hom D  ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) ))
+  1●φBC {a} {b} {c} =  id1 D (F a) ■  {!!}
+  φAB⊗C :  {a b c : Obj C} → Hom D  ( F a ● ( F ( b ⊗ c ) )) (F ( a  ⊗ ( b  ⊗ c )))
+  φAB⊗C {a} {b} {c} =  {!!}
+  φAB●1 :  {a b c : Obj C} → Hom D  ( ( F a ●  F b ) ● F c ) ( F ( a ⊗ b ) ● F c )
+  φAB●1 {a} {b} {c} =  {!!} ■ id1 D (F c)
+  φA⊗BC :  {a b c : Obj C} → Hom D  ( F ( a ⊗ b ) ● F c ) (F ( (a  ⊗  b ) ⊗ c ))
+  φA⊗BC {a} {b} {c} = {!!}
+  FαC : {a b c : Obj C} → Hom D (F ( (a  ⊗  b ) ⊗ c )) (F ( a  ⊗ ( b  ⊗ c )))
+  FαC {a} {b} {c} =  FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) )
+  1●φ : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) )
+  1●φ {a} {b} =  id1 D (F a)  ■  φ 
+  φAIC : { a b : Obj C } → Hom D  ( F a ● F ( Monoidal.m-i M ) ) (F ( a  ⊗ Monoidal.m-i M ))
+  φAIC {a} {b} = {!!}
+  FρC : { a b : Obj C } → Hom D   (F ( a  ⊗ Monoidal.m-i M ))( F a  )
+  FρC {a} {b} = FMap MF (  ≅→ (mρ-iso (isMonoidal M) {a} ) )
+  ρD : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a  )
+  ρD {a} {b} =  ≅→ (mρ-iso (isMonoidal N) {F a} )
+  φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b  ) ( F ( Monoidal.m-i M )  ● F b  )
+  φ●1 {a} {b} =  φ  ■ id1 D (F b)
+  φICB : { a b : Obj C } → Hom D  ( F ( Monoidal.m-i M )  ● F b  ) ( F (  ( Monoidal.m-i M )  ⊗ b ) )
+  φICB {a} {b} = {!!}
+  FλD : { a b : Obj C } → Hom D  ( F (  ( Monoidal.m-i M )  ⊗ b ) ) (F b ) 
+  FλD {a} {b} = FMap MF ( ≅→ (mλ-iso (isMonoidal M) {b} ) )
+  λD : { a b : Obj C } → Hom D  (Monoidal.m-i N ● F b  )  (F b ) 
+  λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} )
   field
      comm1 : {a b c : Obj C } → D [ D [ φAB⊗C {a} {b} {c} o D [ 1●φBC o αD ] ]  ≈ D [ FαC  o  D [ φA⊗BC o φAB●1 ] ] ]
      comm-idr : {a b : Obj C } → D [ D [ FρC  {a} {b}  o D [ φAIC {a} {b} o  1●φ {a} {b} ] ]  ≈ ρD {a} {b}  ]