Edit detail for Limits and Colimits revision 2 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

(1) -> <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/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/limits.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/limits.as", line 2: 
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

)show Product2(Integer,Float)

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      Product2 is not the name of a known type constructor. If you want
      to see information about any operations named Product2 , issue
                        )display operations Product2 

      Integer is not the name of a known type constructor. If you want 
      to see information about any operations named Integer , issue
                         )display operations Integer 

      Float is not the name of a known type constructor. If you want to
      see information about any operations named Float , issue
                          )display operations Float 

)show Product3(Integer,Integer,Integer)

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      Product3 is not the name of a known type constructor. If you want
      to see information about any operations named Product3 , issue
                        )display operations Product3 

      Integer is not the name of a known type constructor. If you want 
      to see information about any operations named Integer , issue
                         )display operations Integer 

      Integer is not the name of a known type constructor. If you want 
      to see information about any operations named Integer , issue
                         )display operations Integer 

      Integer is not the name of a known type constructor. If you want 
      to see information about any operations named Integer , issue
                         )display operations Integer

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)

   There are no library operations named Product2 
      Use HyperDoc Browse or issue
                              )what op Product2
      to learn if there is any operation containing " Product2 " in its
      name.

   Cannot find a definition or applicable library operation named 
      Product2 with argument type(s) 
                                    Type
                                    Type

      Perhaps you should use "@" to indicate the required return type, 
      or "$" to specify which version of the function you need.

#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

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/colimits.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/colimits.as", line 2: 
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

)show Sum2(Integer,Float)

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      Sum2 is not the name of a known type constructor. If you want to 
      see information about any operations named Sum2 , issue
                          )display operations Sum2 

      Integer is not the name of a known type constructor. If you want 
      to see information about any operations named Integer , issue
                         )display operations Integer 

      Float is not the name of a known type constructor. If you want to
      see information about any operations named Float , issue
                          )display operations Float 

)show Sum3(Integer,Float,String)

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      Sum3 is not the name of a known type constructor. If you want to 
      see information about any operations named Sum3 , issue
                          )display operations Sum3 

      Integer is not the name of a known type constructor. If you want 
      to see information about any operations named Integer , issue
                         )display operations Integer 

      Float is not the name of a known type constructor. If you want to
      see information about any operations named Float , issue
                          )display operations Float 

      String is not the name of a known type constructor. If you want 
      to see information about any operations named String , issue
                         )display operations String

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)

   There are no library operations named Sum2 
      Use HyperDoc Browse or issue
                                )what op Sum2
      to learn if there is any operation containing " Sum2 " in its 
      name.

   Cannot find a definition or applicable library operation named Sum2 
      with argument type(s) 
                                    Type
                                    Type

      Perhaps you should use "@" to indicate the required return type, 
      or "$" to specify which version of the function you need.

Note: There is a problem with dependent domains in FriCAS?:

sum(Integer,abs$Integer,wholePart$Float)$Sum2(Integer,Float)

   There are no library operations named Sum2 
      Use HyperDoc Browse or issue
                                )what op Sum2
      to learn if there is any operation containing " Sum2 " in its 
      name.

   Cannot find a definition or applicable library operation named Sum2 
      with argument type(s) 
                                    Type
                                    Type

      Perhaps you should use "@" to indicate the required return type, 
      or "$" to specify which version of the function you need.