|
|
|
last edited 17 years ago by Bill Page |
Edit detail for SandBox Aldor Category Theory 3 revision 1 of 7
| 1 2 3 4 5 6 7 | ||
|
Editor: Bill Page
Time: 2007/11/20 20:20:49 GMT-8 |
||
| Note: | ||
changed: - \begin{aldor} #include "axiom" #pile #library lbasics "basics.ao" import lbasics define Arrow(Obj:Category):Category == with domain: Obj codomain: Obj arrow: domain -> codomain put: (domain,codomain) -> % get: % -> (domain,codomain) Arrow(Obj:Category,A:Obj,B:Obj,f:A->B):Arrow Obj with Set == add domain: Obj == A codomain: Obj == B arrow: domain -> codomain == (x:domain):codomain +-> ( f (x pretend A) ) pretend codomain Rep == domain; import from Rep (x:%)=(y:%):Boolean == if domain has Set then xd:domain == rep x yd:domain == rep y xd = yd else { error "Equality is not defined for this arrow." } (t:TextWriter)<<(x:%):TextWriter == if domain has Set and codomain has Set then import from codomain xd:domain == rep x t << xd << "->" << arrow xd else { error "<< not available for this arrow" } put(a:domain,b:codomain):% == if domain has Set and codomain has Set then if ~(arrow a=b) then error "An arrow square fails to commute." a pretend % get(x:%):(domain,codomain) == ( rep x , arrow rep x ) #if bugs_get_fixed -- the code below causes runtime errors. --- --- Given a category, the domain below supplies a new category where the --- objects are Arrows and the morphisms are 2-morphisms. --- ArrowCategory(Obj:Category,Cat:MathCategory Obj):MathCategory Arrow Obj with if Cat has Final Obj then Final Arrow Obj if Cat has Initial Obj then Initial Arrow Obj == add if Cat has Final Obj then 1:Arrow Obj == Arrow(Obj,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) 1(A:Arrow Obj):(A->1) == (a:A):1 +-> (1$Cat)@Obj pretend 1 if Cat has Initial Obj then 0:Arrow Obj == Arrow(Obj,(0$Cat),(0$Cat),(0$Cat)(0$Cat)) 0(A:Arrow Obj):(0->A) == (z:0):A +-> never -- -- this does also... just try the most obvious thing and it will blow up -- It seems to be compiler problems. (1.1.12p6) -- --ArrowCategory(Cat:MathCategory Set with Final Set):MathCategory Arrow Set with -- Final Arrow Set --== add -- 1:Arrow Set == Arrow(Set,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) -- 1(A:Arrow Set):(A->1) == (a:A):1 +-> (1$Cat)@Set pretend 1 -- #endif \end{aldor}
aldor#include "axiom" #pile #library lbasics "basics.ao" import lbasics define Arrow(Obj:Category):Category == with domain: Obj codomain: Obj arrow: domain -> codomain put: (domain,codomain) -> % get: % -> (domain,codomain) Arrow(Obj:Category,A:Obj,B:Obj,f:A->B):Arrow Obj with Set == add domain: Obj == A codomain: Obj == B arrow: domain -> codomain == (x:domain):codomain +-> ( f (x pretend A) ) pretend codomain Rep == domain; import from Rep (x:%)=(y:%):Boolean == if domain has Set then xd:domain == rep x yd:domain == rep y xd = yd else { error "Equality is not defined for this arrow." } (t:TextWriter)<<(x:%):TextWriter == if domain has Set and codomain has Set then import from codomain xd:domain == rep x t << xd << "->" << arrow xd else { error "<< not available for this arrow" } put(a:domain,b:codomain):% == if domain has Set and codomain has Set then if ~(arrow a=b) then error "An arrow square fails to commute." a pretend % get(x:%):(domain,codomain) == ( rep x , arrow rep x ) #if bugs_get_fixed -- the code below causes runtime errors. --- --- Given a category, the domain below supplies a new category where the --- objects are Arrows and the morphisms are 2-morphisms. --- ArrowCategory(Obj:Category,Cat:MathCategory Obj):MathCategory Arrow Obj with if Cat has Final Obj then Final Arrow Obj if Cat has Initial Obj then Initial Arrow Obj == add if Cat has Final Obj then 1:Arrow Obj == Arrow(Obj,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) 1(A:Arrow Obj):(A->1) == (a:A):1 +-> (1$Cat)@Obj pretend 1 if Cat has Initial Obj then 0:Arrow Obj == Arrow(Obj,(0$Cat),(0$Cat),(0$Cat)(0$Cat)) 0(A:Arrow Obj):(0->A) == (z:0):A +-> never -- -- this does also... just try the most obvious thing and it will blow up -- It seems to be compiler problems. (1.1.12p6) -- --ArrowCategory(Cat:MathCategory Set with Final Set):MathCategory Arrow Set with -- Final Arrow Set --== add -- 1:Arrow Set == Arrow(Set,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) -- 1(A:Arrow Set):(A->1) == (a:A):1 +-> (1$Cat)@Set pretend 1 -- #endif
aldor
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/5541158937811521662-25px001.as using
AXIOM-XL compiler and options
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
Use the system command )set compiler args to change these
options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
"/var/zope2/var/LatexWiki/5541158937811521662-25px001.as", line 4:
import lbasics
.......^
[L4 C8] #2 (Error) Improper form appearing in `import' statement.
Maybe you want to use `import from ...'.
The )library system command was not called after compilation.