--- a/free-monoid.agda	Mon Aug 19 18:14:19 2013 +0900
+++ b/free-monoid.agda	Tue Aug 20 17:57:22 2013 +0900
@@ -68,7 +68,7 @@
   field
       morph : Carrier a -> Carrier b  
       identity     :  morph (ε a)  ≡  ε b
-      mdistr :  ∀{x y} -> morph ( _∙_ a x  y ) ≡ ( _∙_ b (morph  x ) (morph  y) )
+      homo :  ∀{x y} -> morph ( _∙_ a x  y ) ≡ ( _∙_ b (morph  x ) (morph  y) )
 
 open Monomorph
 
@@ -76,25 +76,26 @@
 _+_ {a} {b} {c} f g =  record {
       morph = \x ->  morph  f ( morph g x ) ;
       identity  = identity1 ;
-      mdistr  = mdistr1 
+      homo  = homo1 
    } where
       identity1 : morph f ( morph g (ε a) )  ≡  ε c
       -- morph f (ε b) = ε c ,  morph g (ε a) ) ≡  ε b
       -- morph f  morph g (ε a) ) ≡  morph f (ε b) = ε c
       identity1 = trans ( ≡-cong (morph f ) ( identity g ) )  ( identity f )
-      mdistr1 :  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
+      homo1 :  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
       --  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ morph f ( ( _∙_ c  (morph  g x )) (morph  g y) ) 
-      --  ∀{x y} -> morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
-      mdistr1 = trans  (≡-cong (morph f ) ( mdistr g) ) ( mdistr f ) 
+      --  ∀{x y} -> morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  
+      --         ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
+      homo1 = trans  (≡-cong (morph f ) ( homo g) ) ( homo f ) 
 
 M-id : { a : ≡-Monoid } -> Monomorph a a 
-M-id = record { morph = \x -> x  ; identity = refl ; mdistr = refl }
+M-id = record { morph = \x -> x  ; identity = refl ; homo = refl }
 
 _==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c 
 _==_  f g =  morph f ≡ morph g
 
-isMonoidCategory : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
-isMonoidCategory  = record  { isEquivalence =  isEquivalence1 
+isMonoids : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
+isMonoids  = record  { isEquivalence =  isEquivalence1 
                     ; identityL =  refl
                     ; identityR =  refl
                     ; associative = refl
@@ -110,18 +111,18 @@
              ; sym   = sym
              ; trans = trans
              } 
-MonoidCategory : Category _ _ _
-MonoidCategory  =
+Monoids : Category _ _ _
+Monoids  =
   record { Obj =  ≡-Monoid 
          ; Hom = Monomorph
          ; _o_ = _+_  
          ; _≈_ = _==_
          ; Id  =  M-id
-         ; isCategory = isMonoidCategory 
+         ; isCategory = isMonoids 
            }
 
 A = Sets {c}
-B = MonoidCategory  
+B = Monoids  
 
 open Functor
 
@@ -167,20 +168,20 @@
 solution a b f = record {
          morph = \(l : List a) -> Φ l   ;
          identity = refl ;
-         mdistr = \{x y} -> mdistr1 x y 
+         homo = \{x y} -> homo1 x y 
     } where
         _*_ : Carrier b -> Carrier b -> Carrier b
         _*_  f g = _∙_ b f g
-        mdistr1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
-        mdistr1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
-        mdistr1 (x :: xs) y = let open ≡-Reasoning in 
+        homo1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
+        homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
+        homo1 (x :: xs) y = let open ≡-Reasoning in 
              sym ( begin
                 (Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y)
              ≡⟨⟩
                  ((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y)
              ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
                 (f x) * ( (Φ {a} {b} {f} xs)  * (Φ {a} {b} {f} y) )
-             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (mdistr1 xs y )) ⟩
+             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩
                 (f x) * ( Φ {a} {b} {f} ( xs ++ y ) )
              ≡⟨⟩
                 Φ {a} {b} {f} ( x :: ( xs ++ y ) )
@@ -193,8 +194,8 @@
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
 eta  a = \( x : a ) ->  x :: []
 
--- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming )
-postulate Extensionarity : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
+-- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
+postulate Extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
 
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
 FreeMonoidUniveralMapping = 
@@ -217,7 +218,7 @@
                          ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} {f} [] ) )
                      ≡⟨⟩
                          ( λ (x : a ) →  _∙_ b  ( f x ) ( ε b ) )
-                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (Extensionarity lemma-ext1) ⟩
+                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (Extensionality lemma-ext1) ⟩
                          ( λ (x : a ) →  f x  )
                      ≡⟨⟩
                           f
@@ -227,7 +228,7 @@
         uniquness :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →
              { g :  Hom B (Generator a) b } → (FMap U g) o (eta a )  ≡ f  → B [ solution a b f ≈ g ]
         uniquness {a} {b} {f} {g} eq =  
-                     Extensionarity  ( lemma-ext2 ) where
+                     Extensionality  ( lemma-ext2 ) where
                         lemma-ext2 : ( ∀{ x : List a } -> (morph ( solution a b f)) x  ≡ (morph g) x  )
                         -- (morph ( solution a b f)) []  ≡ (morph g) []  )
                         lemma-ext2 {[]} = let open ≡-Reasoning in
@@ -241,19 +242,19 @@
                         lemma-ext2 {x :: xs}  = let open ≡-Reasoning in
                              begin
                                 (morph ( solution a b f)) ( x :: xs )
-                             ≡⟨ mdistr ( solution a b f) {x :: []} {xs} ⟩
+                             ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩
                                  _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph ( solution a b f)) xs )
                              ≡⟨  ≡-cong ( \ k -> (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 {xs} )   ⟩
                                  _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph g) ( xs ))
                              ≡⟨  ≡-cong ( \k -> ( _∙_ b ( k x ) ((morph g) ( xs )) )) (
                                  begin
                                      ( \x -> (morph ( solution a b f)) ( x :: [] ) )
-                                 ≡⟨ Extensionarity lemma-ext3 ⟩
+                                 ≡⟨ Extensionality lemma-ext3 ⟩
                                      ( \x -> (morph g) ( x :: [] ) )
                                  ∎  
                              ) ⟩
                                  _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs ))
-                             ≡⟨ sym ( mdistr g ) ⟩
+                             ≡⟨ sym ( homo g ) ⟩
                                 (morph g) ( x :: xs )
                              ∎   where
                          lemma-ext3 :  ∀{ x : a } -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )