# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376832630 -32400
# Node ID 34a152235dddeae0efc1b0961e33f996958f1b1f
# Parent  b15c1435cfccb4d7170d2c094965573276dc4a4e
solution of universal mapping for free monoid

diff -r b15c1435cfcc -r 34a152235ddd free-monoid.agda
--- a/free-monoid.agda	Sun Aug 18 22:17:46 2013 +0900
+++ b/free-monoid.agda	Sun Aug 18 22:30:30 2013 +0900
@@ -24,9 +24,6 @@
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-data ListObj : Set where
-  * : ListObj
-
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
 list-id-l : { A : Set c } -> { x : List A } ->  [] ++ x ≡ x
@@ -158,3 +155,23 @@
 Generator : Obj A -> Obj B
 Generator s =  list s
 
+-- η
+
+postulate eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
+
+-- solution
+
+solution : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
+solution = {!!}
+
+FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta 
+FreeMonoidUniveralMapping = 
+    record {
+       _* = solution ; 
+       isUniversalMapping = record {
+             universalMapping = {!!} ; 
+             uniquness = {!!} 
+       }
+    }
+
+