# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376839165 -32400
# Node ID 9a5becd056811d127b6f64223cd8cf9dceac10bf
# Parent  34a152235dddeae0efc1b0961e33f996958f1b1f
um

diff -r 34a152235ddd -r 9a5becd05681 free-monoid.agda
--- a/free-monoid.agda	Sun Aug 18 22:30:30 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 00:19:25 2013 +0900
@@ -164,13 +164,21 @@
 solution : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
 solution = {!!}
 
+universalMapping :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → 
+                             _≈_ A  ( FMap U ( f * ) o  η a ]  ≈ f ]
+universalMapping =   ?
+uniquness :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g :  Hom B (F a) b } → 
+                             A [ A [ FMap U g o  η a ]  ≈ f ] → B [ f * ≈ g ]
+uniquness = ?
+
+
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta 
 FreeMonoidUniveralMapping = 
     record {
        _* = solution ; 
        isUniversalMapping = record {
-             universalMapping = {!!} ; 
-             uniquness = {!!} 
+             universalMapping = universalMapping ; 
+             uniquness = uniquness
        }
     }