Edit detail for SandBox Aldor Category Theory revision 11 of 12

changed:
-Miscellaneous Logical helper functions
-
-\begin{aldor}[basics]
-#include "axiom"
-#pile
-    
-define Domain:Category == with;
-
-+++
-+++  A set is often considered to be a collection with "no duplicate elements."
-+++  Here we have a slightly different definition which is important to 
-+++  understand.  We define a Set to be an arbitrary collection together with
-+++  an equivalence relation "=".  Soon this will be made into a mathematical
-+++  category where the morphisms are "functions", by which we mean maps 
-+++  having the special property that a=a' implies f a = f a'.  This definition
-+++  is more convenient both mathematically and computationally, but you need
-+++  to keep in mind that a set may have duplicate elements.
-+++
-define Set:Category == Join(Domain, Printable) with {
-    =:(%,%) -> Boolean;
-}
-+++
-+++  A Preorder is a collection with reflexive and transitive <=, but without
-+++  necessarily being symmetric (x<=y and y<=x) implying x=y.  Since 
-+++  (x<=y and y<=x) is always an equivalence relation, our definition of 
-+++  "Set" is always satisfied in any case. 
-+++
-define Preorder:Category == Set with {
-    <=: (%,%) -> Boolean;
-    >=: (%,%) -> Boolean;
-    < : (%,%) -> Boolean;
-    > : (%,%) -> Boolean;
-    default {
-        (x:%) =(y:%):Boolean == (x<=y) and (y<=x);
-        (x:%)>=(y:%):Boolean ==  y<=x;
-        (x:%)< (y:%):Boolean == (x<=y) and ~(x=y);
-        (x:%)> (y:%):Boolean == (x>=y) and ~(x=y)
-    }
-}
-
-define TotalOrder:Category == Preorder with {
-    min: (%,%) -> %;
-    max: (%,%) -> %;
-    min: Tuple % -> %;
-    max: Tuple % -> %;
-    default {
-        min(x:%,y:%):% == { x<=y => x; y };
-        max(x:%,y:%):% == { x<=y => y; x };
-        import from List %;
-        min(t:Tuple %):% == associativeProduct(%,min,[t]);
-        max(t:Tuple %):% == associativeProduct(%,max,[t]);
-    }
-}  
-+++
-+++  Countable is the category of collections for which every element in the
-+++  collection can be produced.  This is done by the generator "elements" 
-+++  below.  Note that there is no guarantee that elements will not produce
-+++  "duplicates."  In fact, a Countable may not be a Set, so duplicates may
-+++  have no meaning.  Also, Countable is not guaranteed to terminate.
-+++
-define Countable:Category == with {
-    elements: () -> Generator %
-}
---
---  I'm using an empty function elements() rather than a constant elements
---  to avoid some compiler problems.
---
-+++
-+++  CountablyFinite is the same as Countable except that termination is 
-+++  guaranteed.
-+++
-define CountablyFinite:Category == Countable with
-
-+++
-+++  A "Monoids" is the usual Monoid (we don't use Monoid to avoid clashing
-+++  with axllib): a Set with an associative product (associative relative to
-+++  the equivalence relation of the Set, of course) and a unit.
-+++
-define Monoids:Category == Set with {
-    *: (%,%)            -> %;
-    1:                     %;
-    ^:(%,Integer) -> %;
-    monoidProduct:   Tuple %  -> %;  -- associative product
-    monoidProduct:   List  %  -> %;
-    default {
-        (x:%)^(i:Integer):% == {
-            i=0 => 1;
-            i<0 => error "Monoid negative powers are not defined.";
-            associativeProduct(%,*,x for j:Integer in 1..i)
-        };
-        monoidProduct(t:Tuple %):% == { import from List %; monoidProduct(t) }
-        monoidProduct(l:List %):% == {
-            import from NonNegativeInteger;
-            #l = 0 => 1;
-            associativeProduct(%,*,l);
-        }
-   }
-}  
-      
-+++
-+++  Groups are Groups in the usual mathematical sense.  We use "Groups"
-+++  rather than "Group" to avoid clashing with axllib.  
-+++
-define Groups:Category == Monoids with  {
-    inv: % -> %
-}    
-
-+++
-+++  Printing is a whole area that I'm going to have a nice categorical 
-+++  solution for, but still it is convenient to have a low level Printable
-+++  signature for debugging purposes.
-+++
-define Printable:Category == with {
-    coerce: %    -> OutputForm;
-    coerce: List % -> OutputForm;
-    coerce: Generator % -> OutputForm;
-    default {
-        (t:OutputForm)**(l:List %):OutputForm == {
-            import from Integer;
-            empty? l => t;
-            hconcat(coerce first l, hspace(1)$OutputForm) ** rest l;
-        };
-        coerce(l:List %):OutputForm == empty() ** l;
-        coerce(g:Generator %):OutputForm == {
-            import from List %;
-            empty() ** [x for x in g];
-        }
-    }
-}            
-
-+++
-+++  This evaluates associative products.
-+++
-associativeProduct(T:Type,p:(T,T)->T,g:Generator T):T == {
-    l:List T == [t for t in g];
-    associativeProduct(T,p,l);
-}
-associativeProduct(T:Type,p:(T,T)->T,l:List T):T == {
-    if empty? l then error "Empty product.";
-    mb(t:T,l:List T):T == { empty? l => t; mb( p(t,first l), rest l) };
-    mb(first l,rest l)
-}
-+++
-+++  Evaluates the logical "For all ..." construction
-+++    
-forall?(g:Generator Boolean):Boolean == {
-    q:Boolean := true;
-    for x:Boolean in g repeat { if ~x then { q := false; break } }
-    q
-}
-
-+++
-+++  Evaluates the logical "There exists ..." construction
-+++    
-exists?(g:Generator Boolean):Boolean == {
-    q:Boolean := false;
-    for x:Boolean in g repeat { if x then { q := true; break } };
-    q
-}
-
-+++
-+++  The category of "Maps".  There is no implication that a map is a 
-+++  function in the sense of x=x' => f x = f x'
-+++
-define MapCategory(Obj:Category,A:Obj,B:Obj):Category == with {
-    apply: (%,A) -> B;
-    hom:  (A->B) -> %;
-}
-+++
-+++  One convenient implementation of MapCategory 
-+++
-Map(Obj:Category,A:Obj,B:Obj):MapCategory(Obj,A,B) == add {
-    Rep ==> A->B;
-    apply(f:%,a:A):B == (rep f) a;
-    hom  (f:A->B):% == per f
-}
-+++
-+++  This strange function turns any Type into an Aldor Category
-+++
-define Categorify(T:Type):Category == with {
-    value: T
-}
-+++
-+++  The null function
-+++
-null(A:Type,B:Type):(A->B) == (a:A):B +-> error "Attempt to evaluate the null function."
-
-+++
-+++ A handy package for composition of morphisms.  "o" is meant to suggest morphism composition g "o" f, to be coded "g ** f".
-+++
-o(Obj:Category,A:Obj,B:Obj,C:Obj): with
-    **: (B->C,A->B) -> (A->C)
-== add
-    (g:B->C)**(f:A->B):(A->C) == (a:A):C +-> g f a 
-
-\end{aldor}
-
-Test Funtions
-\begin{aldor}
-#include "axiom"
-#pile
-#library lbasics "basics.ao"
-import from lbasics
-
-T:Domain == add
-S:Set == Integer add
-P:Preorder == Integer add
-TO:TotalOrder == Integer add
---CC:Countable == Integer add
---  import from Integer, Generator(Integer)
---  elements():Generator(Integer) == generator (1..10)
-M:Monoids == Integer add
-G:Groups == Fraction Integer add
-MAPS:MapCategory(SetCategory,Integer,Float) == Map(SetCategory,Integer,Float) add
-INTS:Categorify(Integer) == add
-  value:Integer == 1
-\end{aldor}
-
-\begin{axiom}
-)show T
-)show S
-)show P
-)show TO
---)show CC
-)show MAPS
-)show INTS
-null(PositiveInteger,Float)(1)
-(sin ** cos)$o(SetCategory,EXPR INT,EXPR INT,EXPR INT)
-\end{axiom}
-
-From BillPage Tue Nov 20 19:19:32 -0800 2007
-From: Bill Page
-Date: Tue, 20 Nov 2007 19:19:32 -0800
-Subject: next
-Message-ID: <20071120191932-0800@axiom-wiki.newsynthesis.org>
-
-[SandBox Aldor Category Theory 2]
This project is intended to implement the code and concepts
presented by Saul Youssef in  "Prospects for Category Theory
in Aldor", 2004.

http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf

and the following slides:

http://atlas.bu.edu/~youssef/homepage/talks/categories/categories.html

The original code written by Saul is available here:

http://axiom-wiki.newsynthesis.org/public/london.tar.gz

The following links point to modified source code modules and
tests of the Aldor programs in Axiom. The version of Aldor that
is currently being used here is Rev: 16, Last Changed Date:
2007-11-09 from the Aldor source code repository. The version
of Axiom is currently the FriCAS fork, Rev: 123, Last Changed
Date: 2007-11-08. 

- [SandBox Aldor Category Theory Basics]

- [SandBox Aldor Category Theory Categories]

This links and other information here will be updated as work
continues. If you have some interest in category theory and in
Aldor, I would encourage you to jump in here and help! :-)
Comments on this work would also be greatly appreciated. On
can submit comments just be filling out the comment form below.

Regards,
Bill Page.