Mercurial > hg > Members > kono > Proof > category

diff free-monoid.agda @ 690:3d41a8edbf63

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix universal mapping done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 01:29:47 +0900
parents fb9fc9652c04
children
line wrap: on
line diff
--- a/free-monoid.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/free-monoid.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -234,9 +234,11 @@
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
 eta  a = λ ( x : a ) →  x :: []
 
-FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta
+FreeMonoidUniveralMapping : UniversalMapping A B U 
 FreeMonoidUniveralMapping = 
     record {
+       F = Generator ;
+       η = eta ;
        _* = λ {a b} → λ f → solution a b f ; 
        isUniversalMapping = record {
              universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; 
@@ -343,7 +345,7 @@
 -- Eta          x :: []
 -- Epsiron      morph = Φ
 
-adj = UMAdjunction A B  U Generator eta FreeMonoidUniveralMapping 
+adj = UMAdjunction A B U FreeMonoidUniveralMapping