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

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

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
aldor
   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.

[SandBox Aldor Category Theory 4]?