Product is a limit in the sense of category theory. Given a set of domains
X, Y, ... it constructs a new domain and a function (called project
) from
the new domain to each domain such that for any other domain A and functions
f:A->X, g:A->Y, ... there exists a unique function called their product
from
A into the new domain which commutes with the project functions.
reference
aldor
#pile
#include "axiom"
Product2(X:SetCategory,Y:SetCategory): with
construct: (X,Y) -> %
coerce: % -> OutputForm
product: (A:Type, A->X,A->Y) -> (A->%)
project1: (%) -> X
project2: (%) -> Y
== add
Rep == Record(a:X,b:Y)
import from Rep
--
construct(x:X,y:Y):% == per [x,y]
coerce(x:%):OutputForm ==
bracket([coerce(rep(x).a)$X, coerce(rep(x).b)$Y]$List(OutputForm))
project1(x:%):X == rep(x).a
project2(y:%):Y == rep(y).b
product(A:Type,f:A->X,g:A->Y):(A->%) ==
(x:A):% +-> per [f(x),g(x)]
--
Product3(X:SetCategory,Y:SetCategory,Z:SetCategory): with
construct: (X,Y,Z) -> %
coerce: % -> OutputForm
product: (A:Type, A->X,A->Y,A->Z) -> (A->%)
project1: % -> X
project2: % -> Y
project3: % -> Z
== add
Rep == Record(a:X,b:Y,c:Z)
import from Rep
--
construct(x:X,y:Y,z:Z):% == per [x,y,z]
coerce(x:%):OutputForm ==
bracket([coerce(rep(x).a)$X, coerce(rep(x).b)$Y, coerce(rep(x).c)$Z]$List(OutputForm))
project1(x:%):X == rep(x).a
project2(y:%):Y == rep(y).b
project3(z:%):Z == rep(z).c
product(A:Type,f:A->X,g:A->Y,h:A->Z):(A->%) ==
(x:A):% +-> per [f(x),g(x),h(x)]
aldor
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/limits.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 ./limits.lsp
Issuing )library command for limits
Reading /var/zope2/var/LatexWiki/limits.asy
Product3 is now explicitly exposed in frame initial
Product3 will be automatically loaded when needed from
/var/zope2/var/LatexWiki/limits
Product2 is now explicitly exposed in frame initial
Product2 will be automatically loaded when needed from
/var/zope2/var/LatexWiki/limits
axiom
)show Product2(Integer,Float)
Product2(Integer,Float) is a domain constructor.
Abbreviation for Product2 is Product2
This constructor is exposed in this frame.
Issue )edit limits.as to see algebra source code for Product2
------------------------------- Operations --------------------------------
coerce : % -> OutputForm construct : (Integer,Float) -> %
project1 : % -> Integer project2 : % -> Float
product : (Type,(A -> Integer),(A -> Float)) -> (A -> %)
axiom
)show Product3(Integer,Integer,Integer)
Product3(Integer,Integer,Integer) is a domain constructor.
Abbreviation for Product3 is Product3
This constructor is exposed in this frame.
Issue )edit limits.as to see algebra source code for Product3
------------------------------- Operations --------------------------------
coerce : % -> OutputForm project1 : % -> Integer
project2 : % -> Integer project3 : % -> Integer
construct : (Integer,Integer,Integer) -> %
product : (Type,(A -> Integer),(A -> Integer),(A -> Integer)) -> (A -> %)
Sum is a co-limit in the sense of category theory. Given a set of domains
X, Y, ... it constructs a new domain and a function (called inject
) from
each domain to the new domain such that for any other domain A and functions
f:X->A, g:Y->A, ... there exists a unique function called their sum
from
the new domain into A which commutes with the inject functions.
reference
axiom
p:=[2,3.14]$Product2(Integer,Float)
Type: Product2(Integer,Float)
axiom
q:=[2,3.14,"abc"]$Product3(Integer,Float,String)
Type: Product3(Integer,Float,String)
axiom
r:=["a","b","c"]$Product3(String,String,String)
Type: Product3(String,String,String)
axiom
project3 r
Type: String
aldor
#pile
#include "axiom"
Sum2(X:SetCategory,Y:SetCategory): with
coerce: % -> OutputForm
sum: (A:SetCategory, X->A,Y->A) -> (% -> A)
-- Given two functions, each with one of the domains in this Sum
-- and having a common co-domain A: returns the unique function with
-- domain Sum and co-domain A
inject1: X -> %
inject2: Y -> %
== add
Rep == Union(a:X,b:Y)
import from Rep, Integer
--
coerce(x:%):OutputForm ==
rep(x) case a => sub(coerce(rep(x).a)$X,outputForm 1)
rep(x) case b => sub(coerce(rep(x).b)$Y,outputForm 2)
never
inject1(x:X):% == per [a==x]
inject2(y:Y):% == per [b==y]
sum(A:SetCategory,f:X->A,g:Y->A):(%->A) ==
(x:%):A +->
rep(x) case a => f(rep(x).a)
rep(x) case b => g(rep(x).b)
never
--
Sum3(X:SetCategory,Y:SetCategory,Z:SetCategory): with
coerce: % -> OutputForm
sum: (A:SetCategory, X->A,Y->A,Z->A) -> (% -> A)
-- Given three functions, each with one of the domains in this Sum
-- and having a common co-domain A: returns the unique function with
-- domain Sum and co-domain A
inject1: X -> %
inject2: Y -> %
inject3: Z -> %
== add
Rep == Union(a:X,b:Y,c:Z)
import from Rep, Integer
--
coerce(x:%):OutputForm ==
rep(x) case a => sub(coerce(rep(x).a)$X,outputForm 1)
rep(x) case b => sub(coerce(rep(x).b)$Y,outputForm 2)
rep(x) case c => sub(coerce(rep(x).c)$Z,outputForm 3)
never
inject1(x:X):% == per [a==x]
inject2(y:Y):% == per [b==y]
inject3(z:Z):% == per [c==z]
sum(A:SetCategory,f:X->A,g:Y->A,h:Z->A):(%->A) ==
(x:%):A +->
rep(x) case a => f(rep(x).a)
rep(x) case b => g(rep(x).b)
rep(x) case c => h(rep(x).c)
never
aldor
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/colimits.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 ./colimits.lsp
Issuing )library command for colimits
Reading /var/zope2/var/LatexWiki/colimits.asy
Sum2 is now explicitly exposed in frame initial
Sum2 will be automatically loaded when needed from
/var/zope2/var/LatexWiki/colimits
Sum3 is now explicitly exposed in frame initial
Sum3 will be automatically loaded when needed from
/var/zope2/var/LatexWiki/colimits
axiom
)show Sum2(Integer,Float)
Sum2(Integer,Float) is a domain constructor.
Abbreviation for Sum2 is SUM2
This constructor is exposed in this frame.
Issue )edit colimits.as to see algebra source code for SUM2
------------------------------- Operations --------------------------------
coerce : % -> OutputForm inject1 : Integer -> %
inject2 : Float -> %
sum : (SetCategory,(Integer -> A),(Float -> A)) -> (% -> A)
axiom
)show Sum3(Integer,Float,String)
Sum3(Integer,Float,String) is a domain constructor.
Abbreviation for Sum3 is SUM3
This constructor is exposed in this frame.
Issue )edit colimits.as to see algebra source code for SUM3
------------------------------- Operations --------------------------------
coerce : % -> OutputForm inject1 : Integer -> %
inject2 : Float -> % inject3 : String -> %
sum : (SetCategory,(Integer -> A),(Float -> A),(String -> A)) -> (% -> A)
Limits and co-limits are dual concepts in category theory.
Notice in particular how the construction of Product and
Sum above implement that duality. I am especially interested
in how the duality between rep
and per
is involved in
these constructions.
axiom
inject1(-1)$Sum2(Integer,Float)
Type: Sum2(Integer,Float)
axiom
inject2(-1.1)$Sum2(Integer,Float)
Type: Sum2(Integer,Float)
axiom
inject3("c")$Sum3(String,String,String)
Type: Sum3(String,String,String)
Note: There is a problem with dependent domains in FriCAS?:
axiom
sum(Integer,abs$Integer,wholePart$Float)$Sum2(Integer,Float)
There are 1 exposed and 2 unexposed library operations named sum
having 3 argument(s) but none was determined to be applicable.
Use HyperDoc Browse, or issue
)display op sum
to learn more about the available operations. Perhaps
package-calling the operation or using coercions on the arguments
will allow you to apply the operation.
Cannot find a definition or applicable library operation named sum
with argument type(s)
Domain
(Integer -> Integer)
(Float -> Integer)
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.