fricas
(1) -> <aldor>
#include "axiom"
#pile
#library lBasics "basics.ao"
import from lBasics
#library lMorphisms "morphisms.ao"
import from lMorphisms
#library lAdjoints "adjoints.ao"
import from lAdjoints
#library lCategories "categories.ao"
import from lCategories
+++
+++ Cartesian Closed Categories
+++
define CartesianClosedCategory(Obj:Category):Category == MathCategory Obj with _
Product Obj with _
Exponential Obj
+++
+++ Direct Product of objects and morphisms
+++
define Product(Obj:Category):Category == with
Product: (A:Obj,B:Obj) -> ( AB:Obj, AB->A, AB->B, (X:Obj)->(X->A,X->B)->(X->AB) )
Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
*:(Obj,Obj)-> with Obj
default
Product(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2)) ==
(ab1:Obj,pa1:ab1->A1,pb1:ab1->B1, product1: (X:Obj) -> (X->A1,X->B1) -> (X->ab1)) == Product(A1,B1)
(ab2:Obj,pa2:ab2->A2,pb2:ab2->B2, product2: (X:Obj) -> (X->A2,X->B2) -> (X->ab2)) == Product(A2,B2)
(f:A1->A2)*(g:B1->B2):(ab1->ab2) == product2 ( ab1 )( (x:ab1):A2 +-> f pa1 x, (x:ab1):B2 +-> g pb1 x )
(ab1,ab2,*)
(A:Obj)*(B:Obj): with Obj ==
(AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB)) == Product(A,B)
AB add
+++
+++ Direct Sum
+++
define CoProduct(Obj:Category):Category == with
CoProduct: (A:Obj,B:Obj) -> ( AB:Obj, A->AB, B->AB, (X:Obj)->(A->X,B->X)->(AB->X) )
CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
+:(Obj,Obj)-> with Obj
default
CoProduct(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1)) ==
(ab1:Obj,ia1:A1->ab1,ib1:B1->ab1, sum1: (X:Obj) -> (A1->X,B1->X) -> (ab1->X)) == CoProduct(A1,B1)
(ab2:Obj,ia2:A2->ab2,ib2:B2->ab2, sum2: (X:Obj) -> (A2->X,B2->X) -> (ab2->X)) == CoProduct(A2,B2)
(f:A2->A1)+(g:B2->B1):(ab2->ab1) == sum2 ( ab1 ) ( (x:A2):ab1 +-> ia1 f x, (x:B2):ab1 +-> ib1 g x )
(ab1,ab2,+)
(A:Obj)+(B:Obj): with Obj ==
(AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X)) == CoProduct(A,B)
AB add
+++
+++ Multiple Direct Product of a Single Object
+++
define MultiProduct(Obj:Category):Category == with
Product:(A:Obj,n:Integer) -> (Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
^:(Obj,Integer) -> with Obj
default
(A:Obj)^(n:Integer): with Obj ==
(Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple (X->A))->(X->Prod)) == Product(A,n)
Prod add
+++
+++ Multiple Direct Sum of a Single Object
+++
define CoMultiProduct(Obj:Category):Category == with
CoProduct:(A:Obj,n:Integer) -> ( Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
..:(Obj,Integer) -> with Obj
default
(A:Obj)..(n:Integer): with Obj ==
(Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple (A->X))->(Sum->X)) == CoProduct(A,n)
Sum add</aldor>
fricas
Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1722447487155098788-25px001.as
using Aldor compiler and options
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
Use the system command )set compiler args to change these
options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1722447487155098788-25px001.as", line 1:
#include "axiom"
^
[L1 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.
SandBox Aldor Category Theory 7