Mercurial > hg > Members > kono > Proof > category

changeset 158:9a5becd05681

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
um
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2013 00:19:25 +0900
parents 34a152235ddd
children 0be3e0a49cca
files free-monoid.agda
diffstat 1 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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
        }
     }