Edit detail for Limits and Colimits revision 3 of 5

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

#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)]

   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

)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 -> %)

)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

p:=[2,3.14]$Product2(Integer,Float)

(1)

q:=[2,3.14,"abc"]$Product3(Integer,Float,String)

(2)

r:=["a","b","c"]$Product3(String,String,String)

(3)

project3 r

(4)

#pile
#include "axiom"
Sum2(X:SetCategory,Y:SetCategory): with
    coerce: % -> OutputForm
    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]

-- Note: There is a problem with dependent domains in FriCAS so
-- it is necessary to define 'sum' in a separate package.

Sum2Functions(X:SetCategory,Y:SetCategory,A:SetCategory): with
    sum: (X->A,Y->A) -> (Sum2(X,Y) -> 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
  == add
    -- Requires same Rep as domain Sum2!
    macro rep(x) == x pretend Union(a:X,b:Y)
    import from Union(a:X,b:Y)
    --
    sum(f:X->A,g:Y->A):(Sum2(X,Y)->A) ==
       (x:Sum2(X,Y)):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
    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]

Sum3Functions(X:SetCategory,Y:SetCategory,Z:SetCategory,A:SetCategory): with
    sum: (X->A,Y->A,Z->A) -> (Sum3(X,Y,Z) -> 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
  == add
    -- Requires same Rep as domain Sum3!
    macro rep(x) == x pretend Union(a:X,b:Y,c:Z)
    import from Union(a:X,b:Y,c:Z)
    --
    sum(f:X->A,g:Y->A,h:Z->A):(Sum3(X,Y,Z)->A) ==
       (x:Sum3(X,Y,Z)):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

   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'
"/var/zope2/var/LatexWiki/colimits.as", line 28: 
    macro rep(x) == x pretend Union(a:X,b:Y)
..............^
[L28 C15] #2 (Warning) Definition of macro `rep' hides an outer definition.

"/var/zope2/var/LatexWiki/colimits.as", line 62: 
    macro rep(x) == x pretend Union(a:X,b:Y,c:Z)
..............^
[L62 C15] #3 (Warning) Definition of macro `rep' hides an outer definition.

   Compiling Lisp source code from file ./colimits.lsp
   Issuing )library command for colimits
   Reading /var/zope2/var/LatexWiki/colimits.asy
   Sum2Functions is now explicitly exposed in frame initial 
   Sum2Functions will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/colimits
   Sum2 is now explicitly exposed in frame initial 
   Sum2 will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/colimits
   Sum3Functions is now explicitly exposed in frame initial 
   Sum3Functions 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

)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 -> %                 

)show Sum2Functions(Integer,Float,Integer)

 Sum2Functions(Integer,Float,Integer) is a domain constructor.
 Abbreviation for Sum2Functions is SUM2FUN
 This constructor is exposed in this frame.
 Issue )edit colimits.as to see algebra source code for SUM2FUN 

------------------------------- Operations --------------------------------

 sum : ((Integer -> Integer),(Float -> Integer)) -> (Sum2(Integer,Float) ->
Integer)

)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 -> %

)show Sum3Functions(Integer,Float,String)

   The constructor Sum3Functions takes 4 arguments and you have given
      3  .

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.

inject1(-1)$Sum2(Integer,Float)

(5)

inject2(-1.1)$Sum2(Integer,Float)

(6)

inject3("c")$Sum3(String,String,String)

(7)

f:=sum(abs$Integer,wholePart$Float)$Sum2Functions(Integer,Float,Integer)

(8)

f(inject1(-1)$Sum2(Integer,Float))

(9)

f(inject2(3.14)$Sum2(Integer,Float))

(10)