--- a/free-monoid.agda	Mon Aug 19 04:49:07 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 05:05:04 2013 +0900
@@ -162,6 +162,35 @@
 
 open UniversalMapping
 
+Φ :  {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 ;
+         mdistr = \{x y} -> lemma-fm-1 x y 
+    } where
+        lemma-fm-1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
+        lemma-fm-1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
+        lemma-fm-1 (x :: xs) y = let open ≡-Reasoning in 
+             sym ( begin
+                _∙_ b  (Φ {a} {b} {f} (x :: xs)) (Φ {a} {b} {f} y)
+             ≡⟨⟩
+                _∙_ b ( _∙_ b (f x) (Φ {a} {b} {f} xs)) (Φ {a} {b} {f} y)
+             ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
+                _∙_ b (f x) ( _∙_ b  (Φ {a} {b} {f} xs) (Φ {a} {b} {f} y) )
+             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (lemma-fm-1 xs y )) ⟩
+                _∙_ b (f x) ( Φ {a} {b} {f} ( xs ++ y ) )
+             ≡⟨⟩
+                Φ {a} {b} {f} ( x :: ( xs ++ y ) )
+             ≡⟨⟩
+                Φ {a} {b} {f} ( (x ::  xs) ++ y ) 
+             ≡⟨⟩
+                Φ {a} {b} {f} ((Generator a ∙ x :: xs) y) 
+             ∎ )
+
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
 FreeMonoidUniveralMapping  = 
     record {
@@ -171,38 +200,12 @@
              uniquness = \{a b f} -> uniquness {a} {b} {f}
        }
     } where
-        Φ :  {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 )
-        lemma-fm-1 :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  
-                 (x y : Carrier (Generator a)) → Φ {a} {b} {f} ((Generator a ∙ x) y) ≡ (b ∙ Φ {a} {b} {f} x) (Φ {a} {b} {f} y)
-        lemma-fm-1 {a} {b} {f} [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ {a} {b} {f} y))
-        lemma-fm-1 {a} {b} {f} (x :: xs) y = let open ≡-Reasoning in 
-             sym ( begin
-                _∙_ b  (Φ {a} {b} {f} (x :: xs)) (Φ {a} {b} {f} y)
-             ≡⟨⟩
-                _∙_ b ( _∙_ b (f x) (Φ {a} {b} {f} xs)) (Φ {a} {b} {f} y)
-             ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
-                _∙_ b (f x) ( _∙_ b  (Φ {a} {b} {f} xs) (Φ {a} {b} {f} y) )
-             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (lemma-fm-1 {a} {b} {f} xs y )) ⟩
-                _∙_ b (f x) ( Φ {a} {b} {f} ( xs ++ y ) )
-             ≡⟨⟩
-                Φ {a} {b} {f} ( x :: ( xs ++ y ) )
-             ≡⟨⟩
-                Φ {a} {b} {f} ( (x ::  xs) ++ y ) 
-             ≡⟨⟩
-                Φ {a} {b} {f} ((Generator a ∙ x :: xs) y) 
-             ∎ )
-        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 ;
-                 mdistr = \{x y} -> lemma-fm-1 {a} {b} {f} x y 
-            } 
         universalMapping :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  FMap U ( solution a b f  ) o eta a   ≡ f
         universalMapping {a} {b} {f} = let open ≡-Reasoning in 
                      begin
                          FMap U ( solution a b f ) o eta a   
+                     ≡⟨⟩
+                         ( λ x → Φ (eta a x) )
                      ≡⟨ {!!} ⟩
                          f
                      ∎