--- a/monoidal.agda	Mon Nov 27 14:42:49 2017 +0900
+++ b/monoidal.agda	Tue Nov 28 10:47:05 2017 +0900
@@ -269,6 +269,7 @@
 -- so we postulate this
 --    and we cannot indent postulate ...
 postulate FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) →  ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) →  {h f : Hom C a b } →  {g k : Hom C b c } →  C [  C  [ g o h ]  ≈  C [ k o f ]  ] →  D [ D [ FMap F g o fmap h ]  ≈  D [ fmap k o FMap F f ] ]
+
 UniquenessOfFunctor :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ')  (F : Functor C D)
   {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) )
       → ( {b : Obj C } → D [ fmap  (id1 C b) ≈  id1 D (FObj F b) ] )
@@ -978,4 +979,3 @@
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
 
---