Edit detail for SandBox Aldor Category Theory revision 10 of 12

aldor
#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

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

axiom
)show T
 T  is a domain constructor
 Abbreviation for T is T 
 This constructor is exposed in this frame.
 Issue )edit 7978782401659043526-25px002.as to see algebra source code for T 
------------------------------- Operations --------------------------------
Warning: T is being redefined. T is a domain constructor.
 Abbreviation for T is T 
 This constructor is exposed in this frame.
 Issue )edit 7978782401659043526-25px002.as to see algebra source code for T 
------------------------------- Operations --------------------------------
)show S
 S  is a domain constructor
 Abbreviation for S is S 
 This constructor is exposed in this frame.
 Issue )edit 7978782401659043526-25px002.as to see algebra source code for S 
------------------------------- Operations --------------------------------
 ?=? : (%,%) -> Boolean                coerce : % -> OutputForm
 coerce : List % -> OutputForm        
 ?**? : (OutputForm,List %) -> OutputForm
 coerce : Generator % -> OutputForm
)show P
 P  is a domain constructor
 Abbreviation for P is P 
 This constructor is exposed in this frame.
 Issue )edit 7978782401659043526-25px002.as to see algebra source code for P 
------------------------------- Operations --------------------------------
 ?<? : (%,%) -> Boolean                ?<=? : (%,%) -> Boolean
 ?=? : (%,%) -> Boolean                ?>? : (%,%) -> Boolean
 ?>=? : (%,%) -> Boolean               coerce : % -> OutputForm
 coerce : List % -> OutputForm        
 ?**? : (OutputForm,List %) -> OutputForm
 coerce : Generator % -> OutputForm
)show TO
 TO  is a domain constructor
 Abbreviation for TO is TO 
 This constructor is exposed in this frame.
 Issue )edit 7978782401659043526-25px002.as to see algebra source code for TO 
------------------------------- Operations --------------------------------
 ?<? : (%,%) -> Boolean                ?<=? : (%,%) -> Boolean
 ?=? : (%,%) -> Boolean                ?>? : (%,%) -> Boolean
 ?>=? : (%,%) -> Boolean               coerce : % -> OutputForm
 coerce : List % -> OutputForm         max : (%,%) -> %
 max : Tuple % -> %                    min : (%,%) -> %
 min : Tuple % -> %                   
 ?**? : (OutputForm,List %) -> OutputForm
 coerce : Generator % -> OutputForm
--)show CC
)show MAPS
 MAPS  is a domain constructor
 Abbreviation for MAPS is MAPS 
 This constructor is exposed in this frame.
 Issue )edit 7978782401659043526-25px002.as to see algebra source code for MAPS 
------------------------------- Operations --------------------------------
 apply : (%,Integer) -> Float          hom : (Integer -> Float) -> %
)show INTS
 INTS  is a domain constructor
 Abbreviation for INTS is INTS 
 This constructor is exposed in this frame.
 Issue )edit 7978782401659043526-25px002.as to see algebra source code for INTS 
------------------------------- Operations --------------------------------
 value : () -> Integer                
null(PositiveInteger,Float)(1)
   There are 1 exposed and 1 unexposed library operations named elt 
      having 1 argument(s) but none was determined to be applicable. 
      Use HyperDoc Browse, or issue
                               )display op elt
      to learn more about the available operations. Perhaps 
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.
   Cannot find application of object of type Domain to argument(s) of 
      type(s) 
                               PositiveInteger
(sin ** cos)$o(SetCategory,EXPR INT,EXPR INT,EXPR INT)
   Category, domain or package constructor Category is not available.