Mercurial > hg > Members > kono > Proof > category

diff free-monoid.agda @ 688:a5f2ca67e7c5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix monad/adjunction definition couniversal to limit does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Nov 2017 21:34:58 +0900
parents 06ffcad985ac
children fb9fc9652c04
line wrap: on
line diff
--- a/free-monoid.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/free-monoid.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -199,8 +199,6 @@
 
 -- solution
 
-open UniversalMapping
-
 --   [a,b,c] → f(a) ∙ f(b) ∙ f(c)
 Φ :  {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) →  List a → Carrier b
 Φ {a} {b} f [] = ε b
@@ -236,9 +234,12 @@
 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 
 FreeMonoidUniveralMapping = 
     record {
+       U = U ;
+       F = Generator ;
+       η =  eta ;
        _* = λ {a b} → λ f → solution a b f ; 
        isUniversalMapping = record {
              universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; 
@@ -308,8 +309,9 @@
 
 open NTrans
 --   fm-ε b = Φ
+
 fm-ε :  NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor
-fm-ε =  nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping 
+fm-ε =  nat-ε A B FreeMonoidUniveralMapping 
 --   TMap = λ a  →  solution (FObj U a) a (λ x → x ) ;
 --   isNTrans = record {
 --        commute =  commute1 
@@ -337,8 +339,6 @@
      commute1 {a} {b} {f} =  refl   --    λ (x : a ) → f x :: []
         
 
-open Adjunction
-
 -- A = Sets {c}
 -- B = Monoids  
 -- U   underline funcotr
@@ -346,7 +346,7 @@
 -- Eta          x :: []
 -- Epsiron      morph = Φ
 
-adj = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping 
+adj = UMAdjunction A B FreeMonoidUniveralMapping