login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandBox Aldor Category Theory 3 revision 2 of 7

1 2 3 4 5 6 7
Editor: Bill Page
Time: 2007/11/20 20:25:19 GMT-8
Note:

changed:
-\begin{aldor}
\begin{aldor}[arrow]

changed:
-#library lbasics "basics.ao"
-import lbasics
#library    lBasics  "basics.ao"
import from lBasics

changed:
-    (t:TextWriter)<<(x:%):TextWriter == 
    coerce(x:%):OutputForm == 

added:
            import from List OutputForm


changed:
-            t << xd << "->" << arrow xd
            hconcat [coerce(xd), message "->", coerce arrow xd]

changed:
-            if ~(arrow a=b) then error "An arrow square fails to commute."
            if not(arrow a=b) then error "An arrow square fails to commute."

aldor
#include "axiom" #pile #library lBasics "basics.ao" import from 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." } 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
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/arrow.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'
   Compiling Lisp source code from file ./arrow.lsp
   Issuing )library command for arrow
   Reading /var/zope2/var/LatexWiki/arrow.asy
   Arrow is now explicitly exposed in frame initial 
   Arrow will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/arrow