--- a/monoidal.agda	Sun Nov 26 16:35:22 2017 +0900
+++ b/monoidal.agda	Sun Nov 26 17:12:00 2017 +0900
@@ -499,7 +499,7 @@
   field
       pure  : {a : Obj Sets} → Hom Sets a ( FObj F a )
       <*>   : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
-      --  should have Applicative law
+      --  should have Applicative law ( if we do we have to prove someting more )
 
 lemma1 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative F → HaskellMonoidalFunctor F
 lemma1 F app = record { unit = unit ; φ = φ }
@@ -569,11 +569,11 @@
       --    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
       --    and we cannot indent postulate ...
       postulate FreeTheorem : {l : Level } {a b c : Obj (Sets {l}) } → (F : Functor (Sets {l}) (Sets {l} ) ) →  ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) ) →  {h f : Hom Sets a b } →  {g k : Hom Sets b c } →  Sets [  g o h  ≈  k o f  ] →  Sets [ FMap F g o fmap h  ≈  fmap k o FMap F f  ]
-      UniqunessOfFunctor :   (F : Functor Sets Sets)
+      UniquenessOfFunctor :   (F : Functor Sets Sets)
           {a b : Obj Sets } { f : Hom Sets a b } → ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) )
               → ( {b : Obj Sets } → Sets [ fmap  (id1 Sets b) ≈  id1 Sets (FObj F b) ] )
               → Sets [ fmap f ≈  FMap F f ]
-      UniqunessOfFunctor F {a} {b} {f} fmap eq = begin
+      UniquenessOfFunctor F {a} {b} {f} fmap eq = begin
                 fmap f 
              ≈↑⟨ idL ⟩
                 id1 Sets (FObj F b)  o  fmap f 
@@ -590,7 +590,7 @@
       F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } →  FMap F f x ≡ pure f <*> x
       F→pure {a} {b} {f} {x} = sym ( begin
                  pure f <*> x
-             ≡⟨ ≡-cong ( λ k → k x ) (UniqunessOfFunctor F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x →  IsApplicative.identity ismf  ))) ⟩
+             ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x →  IsApplicative.identity ismf  ))) ⟩
                  FMap F f x
              ∎ )
            where
@@ -598,20 +598,12 @@
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
       p*p : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
       p*p =  IsApplicative.homomorphism ismf
-      car : { a b c : Obj Sets } { f : Hom Sets a (b → c) } { x : a } { y : FObj F b }
-         → ( (pure f <*> pure x ) <*> y ) ≡ ( pure (f x) <*> y ) 
-      car = left ( IsApplicative.homomorphism ismf )
-      cdr : { a b c d : Obj Sets } { f : Hom Sets a c } { x : a } { y : FObj F (c → d) }
-         →  y <*> (pure f <*> pure x )  ≡ y <*> ( pure (f x) )
-      cdr = right ( IsApplicative.homomorphism ismf )
-      cdar : { a b c d : Obj Sets } { f : Hom Sets a (b → c) } { x : a } { y : FObj F b } { y1 : FObj F (c → d) }
-         →  y1 <*> ( (pure f <*> pure x ) <*> y ) ≡ y1 <*> ( pure (f x) <*> y ) 
-      cdar = right ( left ( IsApplicative.homomorphism ismf ) )
-      cadr : { a b c d e : Obj Sets } { f : Hom Sets a c } { x : a } { y : FObj F (c → ( e → a )) } { y1 : FObj F e }
-         →  (y <*> (pure f <*> pure x )) <*> y1  ≡ (y <*> ( pure (f x) )) <*> y1
-      cadr = left (right ( IsApplicative.homomorphism ismf ) )
       comp = IsApplicative.composition ismf
       inter = IsApplicative.interchange ismf
+      pureAssoc :  {a b c : Obj Sets } ( f : b → c ) ( g : a → b ) ( h : FObj F a ) → pure f <*> ( pure g <*> h ) ≡ pure ( f ・ g ) <*> h
+      pureAssoc f g h = trans ( trans (sym comp) (left (left p*p) )) ( left p*p  )
+           where
+                  open Relation.Binary.PropositionalEquality
       comm00 : {a b :  Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b}  (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
          (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
       comm00 {a} {b} {(f , g)} (x , y) = begin