--- a/free-monoid.agda	Sat Mar 29 23:12:12 2014 +0900
+++ b/free-monoid.agda	Thu Apr 17 13:42:57 2014 +0900
@@ -162,35 +162,35 @@
 open UniversalMapping
 
 --   [a,b,c] → f(a) ∙ f(b) ∙ f(c)
-Φ :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  List a → Carrier b
-Φ {a} {b} {f} [] = ε b
-Φ {a} {b} {f} ( x :: xs ) = _∙_ b  ( f x ) (Φ {a} {b} {f} xs )
+Φ :  {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) →  List a → Carrier b
+Φ {a} {b} f [] = ε b
+Φ {a} {b} f ( x :: xs ) = _∙_ b  ( f x ) (Φ {a} {b} f xs )
 
 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
 solution a b f = record {
-         morph = λ (l : List a) → Φ l   ;
-         identity = refl ;
+         morph = λ (l : List a) → Φ f l   ;
+         identity = refl;
          homo = λ {x y} → homo1 x y 
     } where
         _*_ : Carrier b → Carrier b → Carrier b
         _*_  f g = _∙_ b f g
-        homo1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
-        homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
+        homo1 : (x y : Carrier (Generator a)) → Φ f ((Generator a ∙ x) y) ≡ (b ∙ Φ f x) (Φ {a} {b} f y)
+        homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ f y))
         homo1 (x :: xs) y = let open ≡-Reasoning in 
              sym ( begin
-                (Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y)
+                (Φ {a} {b} f (x :: xs)) * (Φ f y)
              ≡⟨⟩
-                 ((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y)
+                 ((f x) * (Φ f xs)) * (Φ f y)
              ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
-                (f x) * ( (Φ {a} {b} {f} xs)  * (Φ {a} {b} {f} y) )
+                (f x) * ( (Φ f xs)  * (Φ f y) )
              ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩
-                (f x) * ( Φ {a} {b} {f} ( xs ++ y ) )
+                (f x) * ( Φ f ( xs ++ y ) )
              ≡⟨⟩
-                Φ {a} {b} {f} ( x :: ( xs ++ y ) )
+                Φ {a} {b} f ( x :: ( xs ++ y ) )
              ≡⟨⟩
-                Φ {a} {b} {f} ( (x ::  xs) ++ y ) 
+                Φ {a} {b} f ( (x ::  xs) ++ y ) 
              ≡⟨⟩
-                Φ {a} {b} {f} ((Generator a ∙ x :: xs) y) 
+                Φ {a} {b} f ((Generator a ∙ x :: xs) y) 
              ∎ )
 
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
@@ -214,11 +214,11 @@
                      begin
                          FMap U ( solution a b f ) o eta a   
                      ≡⟨⟩
-                         ( λ (x : a ) → Φ {a} {b} {f} (eta a x) )
+                         ( λ (x : a ) → Φ {a} {b} f (eta a x) )
                      ≡⟨⟩
-                         ( λ (x : a ) → Φ {a} {b} {f} ( x :: [] ) )
+                         ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) )
                      ≡⟨⟩
-                         ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} {f} [] ) )
+                         ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} f [] ) )
                      ≡⟨⟩
                          ( λ (x : a ) →  _∙_ b  ( f x ) ( ε b ) )
                      ≡⟨ ≡-cong ( λ  g → ( ( λ (x : a ) →  g x ) )) (extensionality {a} lemma-ext1) ⟩