Edit detail for Limits and Colimits revision 1 of 5

changed:
-
**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 <em>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</em>.

"reference":http://en.wikipedia.org/wiki/Product_%28category_theory%29

\begin{aldor}[limits]
#pile
#include "axiom"
Product(X:Type,Y:Type): with
    product: (A:Type, A->X,A->Y) -> (A->%)
    project: % -> X
    project: % -> Y
  == add
    Rep == Record(a:X,b:Y)
    import from Rep
    --
    project(x:%):X == rep(x).a
    project(x:%):Y == rep(x).b
    product(A:Type,f:A->X,g:A->Y):(A->%) ==
       (x:A):% +-> per [f(x),g(x)]
--
Product(X:Type,Y:Type,Z:Type): with
    product: (A:Type, A->X,A->Y,A->Z) -> (A->%)
    project: % -> X
    project: % -> Y
    project: % -> Z
  == add
    Rep == Record(a:X,b:Y,c:Z)
    import from Rep
    --
    project(x:%):X == rep(x).a
    project(x:%):Y == rep(x).b
    project(x:%):Z == rep(x).c
    product(A:Type,f:A->X,g:A->Y,h:A->Z):(A->%) ==
       (x:A):% +-> per [f(x),g(x),h(x)]
\end{aldor}


**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 <em>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</em>.

"reference":http://en.wikipedia.org/wiki/Coproduct

\begin{aldor}[colimits]
#pile
#include "axiom"
Sum(X:Type,Y:Type): with
    sum: (A:Type, 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
    inject: X -> %
    inject: Y -> %
  == add
    Rep == Union(a:X,b:Y)
    import from Rep
    --
    inject(x:X):% == per [a==x]
    inject(y:Y):% == per [b==y]
    sum(A:Type,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
--
Sum(X:Type,Y:Type,Z:Type): with
    sum: (A:Type, 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
    inject: X -> %
    inject: Y -> %
    inject: Z -> %
  == add
    Rep == Union(a:X,b:Y,c:Z)
    import from Rep
    --
    inject(x:X):% == per [a==x]
    inject(y:Y):% == per [b==y]
    inject(z:Z):% == per [c==z]
    sum(A:Type,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
\end{aldor}

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.

#pile
#include "axiom"
Product(X:Type,Y:Type): with
    product: (A:Type, A->X,A->Y) -> (A->%)
    project: % -> X
    project: % -> Y
  == add
    Rep == Record(a:X,b:Y)
    import from Rep
    --
    project(x:%):X == rep(x).a
    project(x:%):Y == rep(x).b
    product(A:Type,f:A->X,g:A->Y):(A->%) ==
       (x:A):% +-> per [f(x),g(x)]
--
Product(X:Type,Y:Type,Z:Type): with
    product: (A:Type, A->X,A->Y,A->Z) -> (A->%)
    project: % -> X
    project: % -> Y
    project: % -> Z
  == add
    Rep == Record(a:X,b:Y,c:Z)
    import from Rep
    --
    project(x:%):X == rep(x).a
    project(x:%):Y == rep(x).b
    project(x:%):Z == rep(x).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
   Product is now explicitly exposed in frame initial 
   Product will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/limits

#pile
#include "axiom"
Sum(X:Type,Y:Type): with
    sum: (A:Type, 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
    inject: X -> %
    inject: Y -> %
  == add
    Rep == Union(a:X,b:Y)
    import from Rep
    --
    inject(x:X):% == per [a==x]
    inject(y:Y):% == per [b==y]
    sum(A:Type,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
--
Sum(X:Type,Y:Type,Z:Type): with
    sum: (A:Type, 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
    inject: X -> %
    inject: Y -> %
    inject: Z -> %
  == add
    Rep == Union(a:X,b:Y,c:Z)
    import from Rep
    --
    inject(x:X):% == per [a==x]
    inject(y:Y):% == per [b==y]
    inject(z:Z):% == per [c==z]
    sum(A:Type,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/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
   Sum is now explicitly exposed in frame initial 
   Sum will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/colimits