# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376855347 -32400
# Node ID c9f29b84ca2f67eec8f5168d18cd5a89257f56d3
# Parent  0be3e0a49cca47733a53fe8cf6d40965ef5ab0ca
hmmm

diff -r 0be3e0a49cca -r c9f29b84ca2f free-monoid.agda
--- a/free-monoid.agda	Mon Aug 19 04:42:06 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 04:49:07 2013 +0900
@@ -165,10 +165,10 @@
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
 FreeMonoidUniveralMapping  = 
     record {
-       _* = \{a b f} solution a b f ; 
+       _* = \{a b} -> \f -> solution a b f ; 
        isUniversalMapping = record {
              universalMapping = \{a b f} -> universalMapping {a} {b} {f} ; 
-             uniquness = \{a b f} uniquness {a} {b} {f}
+             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
@@ -179,34 +179,34 @@
         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  (Φ (x :: xs)) (Φ y)
+                _∙_ b  (Φ {a} {b} {f} (x :: xs)) (Φ {a} {b} {f} y)
              ≡⟨⟩
-                _∙_ b ( _∙_ b (f x) (Φ xs)) (Φ y)
+                _∙_ b ( _∙_ b (f x) (Φ {a} {b} {f} xs)) (Φ {a} {b} {f} y)
              ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
-                _∙_ b (f x) ( _∙_ b  (Φ xs) (Φ y) )
+                _∙_ 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) ( Φ ( xs ++ y ) )
+                _∙_ b (f x) ( Φ {a} {b} {f} ( xs ++ y ) )
              ≡⟨⟩
-                Φ ( x :: ( xs ++ y ) )
+                Φ {a} {b} {f} ( x :: ( xs ++ y ) )
              ≡⟨⟩
-                Φ ( (x ::  xs) ++ y ) 
+                Φ {a} {b} {f} ( (x ::  xs) ++ y ) 
              ≡⟨⟩
-                Φ ((Generator a ∙ 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 x y 
-            }
-        universalMapping :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  FMap U ( solution  f  ) o eta a   ≡ f
+                 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 f ) o eta a   
+                         FMap U ( solution a b f ) o eta a   
                      ≡⟨ {!!} ⟩
                          f
                      ∎ 
         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 f ≈ g ]
+             { g :  Hom B (Generator a) b } → (FMap U g) o (eta a )  ≡ f  → B [ solution a b f ≈ g ]
         uniquness = {!!}