--- a/monoidal.agda	Tue Dec 12 10:25:59 2017 +0900
+++ b/monoidal.agda	Tue Dec 12 10:57:56 2017 +0900
@@ -263,31 +263,6 @@
       ψ  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
       isMonodailFunctor : IsMonoidalFunctor  M N MF ψ
 
------
--- they say it is not possible to prove FreeTheorem in Agda nor Coq
---    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
--- 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) ] )
-      → D [ fmap f ≈  FMap F f ]
-UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin
-        fmap f 
-     ≈↑⟨ idL ⟩
-        id1 D (FObj F b)  o  fmap f 
-     ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
-        FMap F (id1 C b)  o  fmap f 
-     ≈⟨ FreeTheorem C D F  fmap (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory C ))) ⟩ 
-        fmap  (id1 C b)  o  FMap F f  
-     ≈⟨ car eq ⟩
-        id1 D (FObj F b)  o  FMap F f  
-     ≈⟨ idL ⟩
-        FMap F f 
-     ∎  
-   where open ≈-Reasoning D 
 
 open import Category.Sets
 
@@ -366,6 +341,12 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
+----
+--
+--  HaskellMonoidalFunctor is a monoidal functor on Sets
+--
+--
+
 
 record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
       ( unit  : FObj F One )
@@ -396,6 +377,13 @@
       φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
       isHaskellMonoidalFunctor : IsHaskellMonoidalFunctor F unit φ
 
+
+----
+--
+--  laws of HaskellMonoidalFunctor are directly mapped to the laws of Monoidal Functor
+--
+--
+
 HaskellMonoidalFunctor→MonoidalFunctor :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
    → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
 HaskellMonoidalFunctor→MonoidalFunctor {c} F mf = record {
@@ -493,4 +481,4 @@
         Sets [ φ  o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
       comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )
 
-
+-- end