Mercurial > hg > Members > kono > Proof > category

changeset 157:34a152235ddd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
solution of universal mapping for free monoid
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 18 Aug 2013 22:30:30 +0900
parents b15c1435cfcc
children 9a5becd05681
files free-monoid.agda
diffstat 1 files changed, 20 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!} 
+       }
+    }
+
+