Mercurial > hg > Members > kono > Proof > category

changeset 167:c3863043c4a3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Free Monoid and Universal mapping problem done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2013 18:14:19 +0900
parents 2246a7d67ba3
children a9b4132d619b
files free-monoid.agda
diffstat 1 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Mon Aug 19 18:02:52 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 18:14:19 2013 +0900
@@ -1,4 +1,5 @@
--- {-# OPTIONS --universe-polymorphism #-}
+-- Free Monoid and it's Universal Mapping 
+---- using Sets and forgetful functor
 
 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
 
@@ -201,7 +202,7 @@
        _* = \{a b} -> \f -> solution a b f ; 
        isUniversalMapping = record {
              universalMapping = \{a b f} -> universalMapping {a} {b} {f} ; 
-             uniquness = \{a b f} -> uniquness {a} {b} {f}
+             uniquness = \{a b f g} -> uniquness {a} {b} {f} {g}
        }
     } where
         universalMapping :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  FMap U ( solution a b f  ) o eta a   ≡ f
@@ -266,4 +267,11 @@
                              ∎   
 
  
+open import universal-mapping 
 
+adjoint  = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping 
+
+
+ 
+
+