|
|
last edited 17 years ago by Bill Page |
1 2 3 4 5 6 7 | ||
Editor: Bill Page
Time: 2007/11/21 02:41:11 GMT-8 |
||
Note: |
changed: -\begin{aldor}[arrow] \begin{aldor}[slicecategories] changed: - -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." } - coerce(x:%):OutputForm == - if domain has Set and codomain has Set then - import from codomain - import from List OutputForm - - xd:domain == rep x - hconcat [coerce(xd), message "->", coerce arrow xd] - else { error "<< not available for this arrow" } - put(a:domain,b:codomain):% == - if domain has Set and codomain has Set then - if not(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 #library lCategories "categories.ao" import from lCategories +++ +++ Slice Category +++ Slice(Obj:Category,X:Obj):Category == with slice: % -> X SliceCategory(Obj:Category,X:Obj):MathCategory Slice(Obj,X) with Final Slice(Obj,X) == add One():Slice(Obj,X) == W1:Slice(Obj,X) == add Rep == X; import from Rep slice:%->X == (x:%):X +-> rep x W1 add one(A:Slice(Obj,X)):(A->One()) == (a:A):One() +-> (slice a) pretend One() +++ +++ CoSlice Category +++ CoSlice(Obj:Category,X:Obj):Category == with coslice: X -> % CoSliceCategory(Obj:Category,X:Obj):MathCategory CoSlice(Obj,X) with Initial CoSlice(Obj,X) == add Zero():CoSlice(Obj,X) == W2:CoSlice(Obj,X) == add Rep == X coslice:X->% == (x:X):% +-> per x W2 add zero(A:CoSlice(Obj,X)):(Zero()->A) == (z:Zero()):A +-> coslice (z pretend X) +++ +++ The Category of Pairs with pairs of morphisms as morphisms +++ Pair(Obj:Category):Category == with product: % -> (Obj,Obj) product: (Obj,Obj) ->% PairCategory(Obj:Category):MathCategory Pair Obj == add
aldor#include "axiom" #pile #library lBasics "basics.ao" import from lBasics #library lCategories "categories.ao" import from lCategories +++ +++ Slice Category +++ Slice(Obj:Category,X:Obj):Category == with slice: % -> X SliceCategory(Obj:Category,X:Obj):MathCategory Slice(Obj,X) with Final Slice(Obj,X) == add One():Slice(Obj,X) == W1:Slice(Obj,X) == add Rep == X; import from Rep slice:%->X == (x:%):X +-> rep x W1 add one(A:Slice(Obj,X)):(A->One()) == (a:A):One() +-> (slice a) pretend One() +++ +++ CoSlice Category +++ CoSlice(Obj:Category,X:Obj):Category == with coslice: X -> % CoSliceCategory(Obj:Category,X:Obj):MathCategory CoSlice(Obj,X) with Initial CoSlice(Obj,X) == add Zero():CoSlice(Obj,X) == W2:CoSlice(Obj,X) == add Rep == X coslice:X->% == (x:X):% +-> per x W2 add zero(A:CoSlice(Obj,X)):(Zero()->A) == (z:Zero()):A +-> coslice (z pretend X) +++ +++ The Category of Pairs with pairs of morphisms as morphisms +++ Pair(Obj:Category):Category == with product: % -> (Obj,Obj) product: (Obj,Obj) ->% PairCategory(Obj:Category):MathCategory Pair Obj == add
Compiling FriCAS source code from file /var/zope2/var/LatexWiki/slicecategories.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/slicecategories.as", line 14: SliceCategory(Obj:Category,X:Obj):MathCategory Slice(Obj,X) with Final Slice(Obj,X) == add .......................................................................................^ [L14 C88] #2 (Error) The domain is missing some exports. Missing Aut: (A: Slice(Slice(Slice(Slice(Obj, X), X), X), X)) -> Automorphi... Missing End: (A: Slice(Slice(Slice(Slice(Obj, X), X), X), X)) -> Endomorphi... Missing One: () -> Slice(Obj, X) Missing one: (A: Slice(Obj, X)) -> A -> One() "/var/zope2/var/LatexWiki/slicecategories.as", line 28: CoSliceCategory(Obj:Category,X:Obj):MathCategory CoSlice(Obj,X) with Initial CoSlice(Obj,X) == add ...............................................................................................^ [L28 C96] #3 (Error) The domain is missing some exports. Missing Aut: (A: CoSlice(CoSlice(CoSlice(CoSlice(Obj, X), X), X), X)) -> Au... Missing End: (A: CoSlice(CoSlice(CoSlice(CoSlice(Obj, X), X), X), X)) -> En... Missing Zero: () -> CoSlice(Obj, X) Missing zero: (A: CoSlice(Obj, X)) -> Zero() -> A "/var/zope2/var/LatexWiki/slicecategories.as", line 43: PairCategory(Obj:Category):MathCategory Pair Obj == add ....................................................^ [L43 C53] #4 (Error) The domain is missing some exports. Missing Aut: (A: Pair(Pair(Pair(Pair(Obj))))) -> AutomorphismCategory(Pair(... Missing End: (A: Pair(Pair(Pair(Pair(Obj))))) -> EndomorphismCategory(Pair(... The )library system command was not called after compilation.