Edit detail for Limits and Colimits revision 5 of 5

Limits

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

Equalizer is a limit. Given two domains X, Y and two functions f:X->Y, g:X->Y, the Equalizer is a new domain E and a function eq:E->X for which f eq = g eq such that for any other domain M and function m:M->X for which f m = g m, there exists a unique function u:M->E such that u eq = m.

reference

In Spad Equalizer can be defined as a SubDomain as follows:

)abbrev domain EQLZR Equalizer
Equalizer(X:SetCategory,Y:SetCategory,f:X->Y, g:X->Y): SetCategory with
    eq: % -> X
  == SubDomain(X,f #1 = g #1) add
    --
    eq(x:%):X == x pretend X

)abbrev package EQLZF EqualizerFunctions
EqualizerFunctions(X:SetCategory,Y:SetCategory,f:X->Y,g:X->Y, M:SetCategory,m:M->X): with
    u: M->Equalizer(X,Y,f,g)
  == add
    --
    u(x:M):Equalizer(X,Y,f,g) == m(x) pretend Equalizer(X,Y,f,g)

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3871883559109604243-25px003.spad
      using old system compiler.
   EQLZR abbreviates domain Equalizer 
------------------------------------------------------------------------
   initializing NRLIB EQLZR for Equalizer 
   compiling into NRLIB EQLZR 
   compiling exported eq : % -> X
      EQLZR;eq;%X;1 is replaced by x 
Time: 0 SEC.

(time taken in buildFunctor:  0)
Time: 0 SEC.

   Cumulative Statistics for Constructor Equalizer
      Time: 0 seconds

   finalizing NRLIB EQLZR 
   Processing Equalizer for Browser database:
--->-->Equalizer(constructor): Not documented!!!!
--->-->Equalizer((eq (X %))): Not documented!!!!
--->-->Equalizer(): Missing Description
; compiling file "/var/aw/var/LatexWiki/EQLZR.NRLIB/EQLZR.lsp" (written 10 AUG 2025 08:43:28 AM):

; wrote /var/aw/var/LatexWiki/EQLZR.NRLIB/EQLZR.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   Equalizer is now explicitly exposed in frame initial 
   Equalizer will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/EQLZR.NRLIB/EQLZR

   EQLZF abbreviates package EqualizerFunctions 
------------------------------------------------------------------------
   initializing NRLIB EQLZF for EqualizerFunctions 
   compiling into NRLIB EQLZF 
   compiling exported u : M -> Equalizer(X,Y,f,g)
Time: 0 SEC.

(time taken in buildFunctor:  0)
Time: 0 SEC.

   Cumulative Statistics for Constructor EqualizerFunctions
      Time: 0 seconds

   finalizing NRLIB EQLZF 
   Processing EqualizerFunctions for Browser database:
--->-->EqualizerFunctions(constructor): Not documented!!!!
--->-->EqualizerFunctions((u ((Equalizer X Y f g) M))): Not documented!!!!
--->-->EqualizerFunctions(): Missing Description
; compiling file "/var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZF.lsp" (written 10 AUG 2025 08:43:28 AM):

; wrote /var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZF.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   EqualizerFunctions is now explicitly exposed in frame initial 
   EqualizerFunctions will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/EQLZF.NRLIB/EQLZF

)show Equalizer(Float,Float,sin,cos)

 Equalizer(Float,Float,theMap(FLOAT;sin;2%;10,186),theMap(FLOAT;cos;2%;12,186)) is a domain constructor.
 Abbreviation for Equalizer is EQLZR 
 This constructor is exposed in this frame.
 5 names for 5 operations in this domain.
------------------------------- Operations --------------------------------

 ?=? : (%, %) -> Boolean               coerce : % -> OutputForm
 eq : % -> Float                       latex : % -> String
 ?~=? : (%, %) -> Boolean

Co-limits

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
    inject1: X -> %
    coerce: X -> %
    inject2: Y -> %
    coerce: 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]
    coerce(x:X):% == per [a==x]
    inject2(y:Y):% == per [b==y]
    coerce(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 -> %
    coerce: X -> %
    inject2: Y -> %
    coerce: Y -> %
    inject3: Z -> %
    coerce: 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]
    coerce(x:X):% == per [a==x]
    inject2(y:Y):% == per [b==y]
    coerce(y:Y):% == per [b==y]
    inject3(z:Z):% == per [c==z]
    coerce(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/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 Sum2Functions(Integer,Float,Integer)

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

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

      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 

      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 

)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 

)show Sum3Functions(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 .

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

      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.

f:Sum2(Integer,Float)->Integer:=sum(abs$Integer,wholePart$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.