Edit detail for SandBox Aldor Category Theory Categories revision 1 of 2

changed:
-
\begin{aldor}[categories]
#include "axiom"
#pile

#library    lBasics  "basics.ao"
import from lBasics
       
+++
+++  Adjoint functors  Left -| Right
+++
+++  << and >> are the left and right adjunctions: they are the defining isomorphism
+++
+++    Hom(Left A,B) << >> Hom( A, Right B)
+++
+++  unit and counit are the equivalent natural transformations.  left and right are the 
+++  action of the Left and Right functors on the arrows.  unit, counit, left and right are 
+++  provided by default.
+++
define Adjoint(ObjA:Category,ObjB:Category, Left:ObjA->ObjB, Right:ObjB->ObjA):Category == with  {
    >>: (A:ObjA,B:ObjB,  Left A ->       B ) -> (      A -> Right B );  -- 1/2 of the adj. isomorphism
    <<: (A:ObjA,B:ObjB,       A -> Right B ) -> ( Left A ->       B );  -- 2/2 of the adj. isomorphism
    
    unit:   (A:ObjA) -> (           A -> Right  Left A);    --   unit natural transformation
    counit: (B:ObjB) -> (Left Right B ->             B);    -- counit natural transformation
    
    left:  (X:ObjA,Y:ObjA,X->Y) -> (  Left X ->  Left Y );  --  Left functor action on morphisms
    right: (X:ObjB,Y:ObjB,X->Y) -> ( Right X -> Right Y );  -- Right functor action on morphisms
    default  {
        unit  (A:ObjA):(A -> Right Left A)               == >>(      A,Left A,(l:Left  A):Left  A +-> l);
        counit(B:ObjB):(Left Right B -> B)               == <<(Right B,     B,(r:Right B):Right B +-> r);
        left (X:ObjA,Y:ObjA,f:X->Y):( Left X -> Left  Y) == <<(      X,Left Y,(x:           X):Right Left Y +->     unit(Y)(f x));
        right(X:ObjB,Y:ObjB,f:X->Y):(Right X -> Right Y) == >>(Right X,     Y,(x:Left Right X):           Y +-> f counit(X)(x) )
    }
}
+++
+++  The right adjoint of Left
+++
define RightAdjoint(ObjA:Category,ObjB:Category,Left:ObjA->ObjB):Category == with {
    Right: ObjB -> ObjA;
    Adjoint(ObjA,ObjB,Left,Right)
}
+++
+++  The left adjoint of Right
+++    
define LeftAdjoint(ObjA:Category,ObjB:Category,Right:ObjB->ObjA):Category == with {
    Left:  ObjA -> ObjB;
    Adjoint(ObjA,ObjB,Left,Right)
}
+++
+++  Free construction
+++
define FreeConstruction(ObjA:Category,ObjB:Category,Forget:ObjB->ObjA):Category == LeftAdjoint(ObjA,ObjB,Forget) with 

--LeftCategory(ObjA:Category,CatA:MathCategory ObjA, ObjB:Category,  Left:ObjA->ObjB,  Ad:RightAdjoint(ObjA,ObjB,Left)):_
--     MathCategory ObjB with {
--         if   CatA    has      Initial ObjA  then       Initial ObjB;
--         if   CatA    has    CoProduct ObjA  then     CoProduct ObjB;
--         if   CatA    has  CoEqualizer ObjA  then   CoEqualizer ObjB;
--         if   CatA    has      Pushout ObjA  then       Pushout ObjB;
--} == add {
--    if CatA has Initial ObjA then {
--        Zero():ObjB == {
--            LC0:ObjB == Left Zero() add;
--            LC0 add
--        }
--        zero(A:ObjB):(Zero()->A) == {
--            A1:ObjA == (Right$Ad) A;
--            z:(Zero$CatA)()->A1 == (zero$CatA)(A1);
--            
--            error " "
--        }
--    }
--    if CatA has CoProduct ObjA then {
--        CoProduct(A:ObjB,B:ObjB):(AB:ObjB,A->AB,B->AB,(X:ObjB)->(A->X,B->X)->(AB->X)) == {
--            A1:ObjA == (Right$Ad) A;
--            B1:ObjA == (Right$Ad) B;
--            (AB1:ObjA,ia1:A1->AB1,ib1:B1->AB1,coproduct1:(X1:ObjA)->(A1->X1,B1->X1)->(AB1->X1)) == (CoProduct$CatA)(A1,B1);
--            error " "
--        }
--    }
--}

--define LeftCategory(ObjA:Category,CatA:MathCategory ObjA,  ObjB:Category,Left:ObjA->ObjB, _
--          Ad:RightAdjoint(ObjA,ObjB,Left)):Category == with {
--    if   CatA    has      Initial ObjA  then     Initial ObjB;
--    if   CatA    has    CoProduct ObjA  then   CoProduct ObjB;
--    if   CatA    has  CoEqualizer ObjA  then CoEqualizer ObjB;
--    if   CatA    has      Pushout ObjA  then     Pushout ObjB;
--}
--default {
--    if CatA has Initial ObjA then {
--        Zero():ObjB == {
--            LC0:ObjB == Left Zero() add;
--            LC0 add
--        }
--    }
--}

-------  this won't work due to bugs in 1.1.12p6
--+++
--+++  Adjoint in general from ObjA to ObjB
--+++
--define Adjoint(ObjA:Category,ObjB:Category):Category == with
--    Left:  ObjA -> ObjB
--    Right: ObjB -> ObjA
--    Adjoint(ObjA,ObjB,Left,Right)
--
--+++
--+++  Free construction via a forgetful functor.  This is an adjoint with
--+++  conventional renaming.
--+++
--define FreeConstruction(ObjA:Category,ObjB:Category):Category == with
--    Free:   ObjA -> ObjB
--    Free:   (X:ObjA,Y:ObjA,X->Y) -> (Free X -> Free Y)
--    Forget: ObjB -> ObjA 
--    Forget: (X:ObjB,Y:ObjB,X->Y) -> (Forget X -> Forget Y)
--    Adjoint(ObjA,ObjB,Free,Forget)
--    default
--        Free  (X:Domain,Y:Domain,f:X->Y):(Free X->Free Y) == left(X,Y,f)
--        Forget(X:Set,Y:Set,f:X->Y):(Forget X->Forget Y) == right(X,Y,f)

define Arrow(Obj:Category):Category == with 
    domain:    Obj
    codomain:  Obj
    arrow:  domain -> codomain
    put:      (domain,codomain) -> %
    get: % -> (domain,codomain) 


Arrow(Obj:Category,A:Obj,B:Obj,f:A->B):Arrow Obj with Set == add 
    domain:   Obj == A
    codomain: Obj == B
    arrow: domain -> codomain == (x:domain):codomain +-> ( f (x pretend A) ) pretend codomain
    Rep == domain; import from Rep

    (x:%)=(y:%):Boolean == 
        if domain has Set then 
            xd:domain == rep x
            yd:domain == rep y
            xd = yd
        else { error "Equality is not defined for this arrow." }
    coerce(x:%):OutputForm == 
        if domain has Set and codomain has Set then 
            import from codomain
            import from List OutputForm

            xd:domain == rep x
            hconcat [coerce(xd), message "->", coerce arrow xd]
        else { error "<< not available for this arrow" }
    put(a:domain,b:codomain):% == 
        if domain has Set and codomain has Set then 
            if not(arrow a=b) then error "An arrow square fails to commute."
        a pretend %
    get(x:%):(domain,codomain) == ( rep x , arrow rep x )

    
#if bugs_get_fixed
--   the code below causes runtime errors.
---
---  Given a category, the domain below supplies a new category where the
---  objects are Arrows and the morphisms are 2-morphisms.
---
ArrowCategory(Obj:Category,Cat:MathCategory Obj):MathCategory Arrow Obj with
    if Cat has     Final Obj then     Final Arrow Obj  
    if Cat has   Initial Obj then   Initial Arrow Obj
== add
    if Cat has   Final Obj then
        1:Arrow Obj == Arrow(Obj,(1$Cat),(1$Cat),(1$Cat)(1$Cat))
        1(A:Arrow Obj):(A->1) == (a:A):1 +-> (1$Cat)@Obj pretend 1
    if Cat has Initial Obj then
        0:Arrow Obj == Arrow(Obj,(0$Cat),(0$Cat),(0$Cat)(0$Cat))
        0(A:Arrow Obj):(0->A) == (z:0):A +-> never
--
-- this does also...  just try the most obvious thing and it will blow up
-- It seems to be compiler problems. (1.1.12p6)
--
--ArrowCategory(Cat:MathCategory Set with Final Set):MathCategory Arrow Set with 
--    Final Arrow Set
--== add
--    1:Arrow Set == Arrow(Set,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) 
--    1(A:Arrow Set):(A->1) == (a:A):1 +-> (1$Cat)@Set pretend 1
--
#endif

define AutomorphismCategory(Obj:Category,A:Obj):Category == Groups with
    aut:     (A->A,A->A) -> %  -- create an automorphism from a morphism and it's inverse
    aut: % ->(A->A,A->A)       -- create a morphism and it's inverse from an automorphism

+++
+++  If X is an object in any category, Aut X given below is the group
+++  of automorphisms.  If the category has Set and CountablyInfinite, 
+++  autmorphisms are said to be equal if they have equal values at each
+++  point in their domain.
+++
define Automorphism(Obj:Category):Category == with
    Aut: (A:Obj) -> AutomorphismCategory (Obj,A)
    default
        Aut(A:Obj):AutomorphismCategory(Obj,A) == 
	    WW0:AutomorphismCategory(Obj,A) == add
	        Rep == Record(iso:A->A,isi:A->A); import from Rep
	        1:% == per [(a:A):A +-> a, (a:A):A +-> a]
                (x:%)=(y:%):Boolean == 
                     A has CountablyFinite with Set => 
                         import from A
                         forall? ( ((rep x).iso)(a) = ((rep y).iso)(a) for a in (elements$A)() )
                     error "Equality is not available for these automorphisms."
	        import from o(Obj,A,A,A)
	        (g:%)*(f:%):% == per [ ((rep g).iso) ** ((rep f).iso) , ((rep f).isi) ** ((rep g).isi) ]
	        inv(f:%):% == per [ (rep f).isi, (rep f).iso ]
	        aut(isomorphism:A->A,isomorphismInverse:A->A):% == per [isomorphism,isomorphismInverse]
	        aut(f:%):(A->A,A->A) == explode rep f 
                coerce(f:%):OutputForm == message "[Automorphism]"
	    WW0 add
	    
define EndomorphismCategory(Obj:Category,A:Obj):Category == Monoids with
    end:        (A->A) -> %  -- create an endomorphisms from a morphism
    end:   % -> (A->A)       -- create a morphism from an endomorphism

+++
+++  If X is an object in any category, End X given below is the monoid
+++  of endomorphisms.  If the category has Set and CountablyInfinite,
+++  endomorphisms are computed to be equal if they have equal values at
+++  each point in their domain.
+++
define Endomorphism(Obj:Category):Category == with
    End: (A:Obj) -> EndomorphismCategory(Obj,A) 
    default
        End(A:Obj):EndomorphismCategory(Obj,A) == 
	    WW1:EndomorphismCategory(Obj,A) == add
                Rep ==> A->A
	        1:% == per ( (a:A):A +-> a )
	        import from o(Obj,A,A,A)
                (x:%)=(y:%):Boolean == 
                    A has CountablyFinite with Set => 
                        import from A
                        forall? ( (rep x) a = (rep y) a for a in (elements$A)() )
                    error "Equality is not available for endomorphisms."
	        (g:%)*(f:%):% == per ( (rep g)**(rep f) )
	        end(f:A->A):% == per f
	        end(f:%):(A->A) == rep f
                coerce(f:%):OutputForm == message "[Endomorphism]"
	    WW1 add

define Morphisms(Obj:Category):Category == Join(Automorphism Obj, Endomorphism Obj)

+++
+++  The Aldor category of mathematical categories
+++
define MathCategory(Obj:Category):Category == Join(Id Obj, Compose Obj, Morphisms Obj)

+++
+++  One sometimes needs the Hom-style categories where morphisms from A to B
+++  are objects in Hom(A,B) rather than A->B.
+++
define MathCategory(Obj:Category,Hom:(Obj,Obj)->Domains):Category == with 
    id: (A:Obj) -> Hom(A,A)
    compose: (A:Obj,B:Obj,C:Obj) -> (Hom(A,B),Hom(B,C)) -> Hom(A,C)


+++
+++  Identities
+++
define Id(Obj:Category):Category == with
    id: (A:Obj) -> (A->A)
    default
       id(A:Obj):(A->A) == (a:A):A +-> a
       
+++
+++  Composition of Morphisms
+++   
define Compose(Obj:Category):Category == with
    compose: (A:Obj,B:Obj,C:Obj) -> (A->B,B->C) -> (A->C)
    default
        compose(A:Obj,B:Obj,C:Obj)(f:A->B,g:B->C):(A->C) == (a:A):C +-> g f a

+++
+++  Initial Objects
+++    
define Initial(Obj:Category):Category == with
    Zero: () -> Obj
    zero: (A:Obj) -> (Zero()->A)
--    0: Obj
--    0: (A:Obj)->(0->A)

+++
+++  Final Objects
+++    
define Final(Obj:Category):Category == with
    One: () -> Obj
    one: (A:Obj) -> (A->One())
--    1: Obj
--    1: (A:Obj)->(A->1)   

               
+++
+++   Equalizer
+++    
define Equalizer(Obj:Category):Category == with
    Equalizer:   (A:Obj,B:Obj,A->B,A->B) -> (E:Obj,E->A)

+++
+++   CoEqualizer
+++    
define CoEqualizer(Obj:Category):Category == with
    CoEqualizer: (A:Obj,B:Obj,B->A,B->A) -> (E:Obj,A->E)

+++
+++   Pullback Square
+++    
define Pullback(Obj:Category):Category == with
    Pullback: (A:Obj,C:Obj,B:Obj) -> (A->C,B->C) -> ( Pullback:Obj, Pullback->A,Pullback->B,(X:Obj,X->A,X->B) -> (X->Pullback))

+++
+++   Pushout Square, the dual of a Pullback Square
+++    
define Pushout(Obj:Category):Category == with
    Pushout:  (A:Obj,C:Obj,B:Obj) -> (C->A,C->B) -> ( Pushout:Obj, A->Pushout,B->Pushout, (X:Obj,A->X,A->X) -> ( Pushout->X))

+++
+++   Exponential object
+++
define Exp(Obj:Category,E:Obj):Category == with
    rightProductFunctor: Obj -> Obj
    expFunctor:          Obj -> Obj
    Adjoint(Obj,Obj,rightProductFunctor,expFunctor)

define Exponential(Obj:Category):Category == with
    Exp: (E:Obj) -> Exp(Obj,E)
            
define Hom(Obj:Category):Category == with 
    Hom: (Obj,Obj) -> Obj

define Hom?(Obj:Category):Category == with
    hom?: (Obj,Obj) -> Boolean  -- hom?(A,B) answers "Are there any Homs from A to B?"

+++
+++   Decategorification
+++
define Isomorphic(Obj:Category):Category == with
    isomorphic?: (A:Obj,B:Obj) -> Boolean
    Decategorify: Set with { object: Obj -> % }
    default
        Decategorify: Set with { object: Obj -> % } == add
            Rep == Obj
            object(A:Obj):% == per A
            (A:%)=(B:%):Boolean == isomorphic? ( rep A, rep B)
            coerce(A:%):OutputForm == message "[Object]"

+++
+++  Cartesian Closed Categories
+++
define CartesianClosedCategory(Obj:Category):Category == MathCategory Obj with _
                                                              Product Obj with _
                                                          Exponential Obj 
+++
+++  Direct Product of objects and morphisms
+++	
define Product(Obj:Category):Category == with
    Product: (A:Obj,B:Obj) -> ( AB:Obj, AB->A, AB->B, (X:Obj)->(X->A,X->B)->(X->AB) )
    Product: (A1:Obj,B1:Obj,  A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
    *:(Obj,Obj)-> with Obj
    default
        Product(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2)) ==
	    (ab1:Obj,pa1:ab1->A1,pb1:ab1->B1, product1: (X:Obj) -> (X->A1,X->B1) -> (X->ab1)) == Product(A1,B1)
	    (ab2:Obj,pa2:ab2->A2,pb2:ab2->B2, product2: (X:Obj) -> (X->A2,X->B2) -> (X->ab2)) == Product(A2,B2)
	    (f:A1->A2)*(g:B1->B2):(ab1->ab2) == product2 ( ab1 )( (x:ab1):A2 +-> f pa1 x, (x:ab1):B2 +-> g pb1 x )
	    (ab1,ab2,*)
        (A:Obj)*(B:Obj): with Obj == 
            (AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB)) == Product(A,B)
            AB add
        
+++
+++  Direct Sum
+++
define CoProduct(Obj:Category):Category == with
    CoProduct: (A:Obj,B:Obj) -> ( AB:Obj, A->AB, B->AB, (X:Obj)->(A->X,B->X)->(AB->X) )
    CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
    +:(Obj,Obj)-> with Obj
    default
        CoProduct(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1)) == 
	    (ab1:Obj,ia1:A1->ab1,ib1:B1->ab1, sum1: (X:Obj) -> (A1->X,B1->X) -> (ab1->X)) == CoProduct(A1,B1)
	    (ab2:Obj,ia2:A2->ab2,ib2:B2->ab2, sum2: (X:Obj) -> (A2->X,B2->X) -> (ab2->X)) == CoProduct(A2,B2)
	    (f:A2->A1)+(g:B2->B1):(ab2->ab1) == sum2 ( ab1 ) ( (x:A2):ab1 +-> ia1 f x, (x:B2):ab1 +-> ib1 g x )
	    (ab1,ab2,+)
        (A:Obj)+(B:Obj): with Obj == 
            (AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X)) == CoProduct(A,B)
            AB add
            
+++
+++  Multiple Direct Product of a Single Object
+++    
define MultiProduct(Obj:Category):Category == with
    Product:(A:Obj,n:Integer)   -> (Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
    ^:(Obj,Integer) -> with Obj
    default
        (A:Obj)^(n:Integer): with Obj ==
	    (Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple (X->A))->(X->Prod)) == Product(A,n)
	    Prod add

+++
+++  Multiple Direct Sum of a Single Object
+++	    
define CoMultiProduct(Obj:Category):Category == with
    CoProduct:(A:Obj,n:Integer) -> ( Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
    ..:(Obj,Integer) -> with Obj
    default
        (A:Obj)..(n:Integer): with Obj == 
	    (Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple (A->X))->(Sum->X)) == CoProduct(A,n)
	    Sum add

+++
+++  Quotients
+++ 
define Quotient(Obj:Category):Category == with
    Quotient:  (A:Obj,B:Obj) -> (A->B) -> (Quo:Obj,A->Quo,(X:Obj)->(A->X)->(Quo->X))
    /:(A:Obj,B:Obj) -> ((A->B)->Obj)
    default
        (A:Obj)/(B:Obj):((A->B)->Obj) ==
	    F(f:A->B):Obj == 
	        (Q:Obj,insert:A->Q,quo:(X:Obj)->(A->X)->(Q->X)) == Quotient(A,B)(f)
		Q add
            F

+++
+++   Subobjects (the dual of Quotients)
+++    
define Subobject(Obj:Category):Category == with
    Subobject: (A:Obj,B:Obj) -> (B->A) -> (Sub:Obj,Sub->A,(X:Obj)->(X->A)->(X->Sub))
    \:(A:Obj,B:Obj) -> ((B->A)->Obj)
    default
        (A:Obj)\(B:Obj):(B->A)->Obj ==
	    F(f:(B->A)): Obj ==
	        (S:Obj,include:S->A,sub:(X:Obj)->(X->A)->(X->S)) == Subobject(A,B)(f)
		S add
            F
  
\end{aldor}

From BillPage Tue Nov 20 20:18:38 -0800 2007
From: Bill Page
Date: Tue, 20 Nov 2007 20:18:38 -0800
Subject: 
Message-ID: <20071120201838-0800@axiom-wiki.newsynthesis.org>

[SandBox Aldor Category Theory 3]

aldor
#include "axiom"
#pile
#library    lBasics  "basics.ao"
import from lBasics
+++
+++  Adjoint functors  Left -| Right
+++
+++  << and >> are the left and right adjunctions: they are the defining isomorphism
+++
+++    Hom(Left A,B) << >> Hom( A, Right B)
+++
+++  unit and counit are the equivalent natural transformations.  left and right are the 
+++  action of the Left and Right functors on the arrows.  unit, counit, left and right are 
+++  provided by default.
+++
define Adjoint(ObjA:Category,ObjB:Category, Left:ObjA->ObjB, Right:ObjB->ObjA):Category == with  {
    >>: (A:ObjA,B:ObjB,  Left A ->       B ) -> (      A -> Right B );  -- 1/2 of the adj. isomorphism
    <<: (A:ObjA,B:ObjB,       A -> Right B ) -> ( Left A ->       B );  -- 2/2 of the adj. isomorphism
    unit:   (A:ObjA) -> (           A -> Right  Left A);    --   unit natural transformation
    counit: (B:ObjB) -> (Left Right B ->             B);    -- counit natural transformation
    left:  (X:ObjA,Y:ObjA,X->Y) -> (  Left X ->  Left Y );  --  Left functor action on morphisms
    right: (X:ObjB,Y:ObjB,X->Y) -> ( Right X -> Right Y );  -- Right functor action on morphisms
    default  {
        unit  (A:ObjA):(A -> Right Left A)               == >>(      A,Left A,(l:Left  A):Left  A +-> l);
        counit(B:ObjB):(Left Right B -> B)               == <<(Right B,     B,(r:Right B):Right B +-> r);
        left (X:ObjA,Y:ObjA,f:X->Y):( Left X -> Left  Y) == <<(      X,Left Y,(x:           X):Right Left Y +->     unit(Y)(f x));
        right(X:ObjB,Y:ObjB,f:X->Y):(Right X -> Right Y) == >>(Right X,     Y,(x:Left Right X):           Y +-> f counit(X)(x) )
    }
}
+++
+++  The right adjoint of Left
+++
define RightAdjoint(ObjA:Category,ObjB:Category,Left:ObjA->ObjB):Category == with {
    Right: ObjB -> ObjA;
    Adjoint(ObjA,ObjB,Left,Right)
}
+++
+++  The left adjoint of Right
+++    
define LeftAdjoint(ObjA:Category,ObjB:Category,Right:ObjB->ObjA):Category == with {
    Left:  ObjA -> ObjB;
    Adjoint(ObjA,ObjB,Left,Right)
}
+++
+++  Free construction
+++
define FreeConstruction(ObjA:Category,ObjB:Category,Forget:ObjB->ObjA):Category == LeftAdjoint(ObjA,ObjB,Forget) with 
--LeftCategory(ObjA:Category,CatA:MathCategory ObjA, ObjB:Category,  Left:ObjA->ObjB,  Ad:RightAdjoint(ObjA,ObjB,Left)):_
--     MathCategory ObjB with {
--         if   CatA    has      Initial ObjA  then       Initial ObjB;
--         if   CatA    has    CoProduct ObjA  then     CoProduct ObjB;
--         if   CatA    has  CoEqualizer ObjA  then   CoEqualizer ObjB;
--         if   CatA    has      Pushout ObjA  then       Pushout ObjB;
--} == add {
--    if CatA has Initial ObjA then {
--        Zero():ObjB == {
--            LC0:ObjB == Left Zero() add;
--            LC0 add
--        }
--        zero(A:ObjB):(Zero()->A) == {
--            A1:ObjA == (Right$Ad) A;
--            z:(Zero$CatA)()->A1 == (zero$CatA)(A1);
--            
--            error " "
--        }
--    }
--    if CatA has CoProduct ObjA then {
--        CoProduct(A:ObjB,B:ObjB):(AB:ObjB,A->AB,B->AB,(X:ObjB)->(A->X,B->X)->(AB->X)) == {
--            A1:ObjA == (Right$Ad) A;
--            B1:ObjA == (Right$Ad) B;
--            (AB1:ObjA,ia1:A1->AB1,ib1:B1->AB1,coproduct1:(X1:ObjA)->(A1->X1,B1->X1)->(AB1->X1)) == (CoProduct$CatA)(A1,B1);
--            error " "
--        }
--    }
--}
--define LeftCategory(ObjA:Category,CatA:MathCategory ObjA,  ObjB:Category,Left:ObjA->ObjB, _
--          Ad:RightAdjoint(ObjA,ObjB,Left)):Category == with {
--    if   CatA    has      Initial ObjA  then     Initial ObjB;
--    if   CatA    has    CoProduct ObjA  then   CoProduct ObjB;
--    if   CatA    has  CoEqualizer ObjA  then CoEqualizer ObjB;
--    if   CatA    has      Pushout ObjA  then     Pushout ObjB;
--}
--default {
--    if CatA has Initial ObjA then {
--        Zero():ObjB == {
--            LC0:ObjB == Left Zero() add;
--            LC0 add
--        }
--    }
--}
-------  this won't work due to bugs in 1.1.12p6
--+++
--+++  Adjoint in general from ObjA to ObjB
--+++
--define Adjoint(ObjA:Category,ObjB:Category):Category == with
--    Left:  ObjA -> ObjB
--    Right: ObjB -> ObjA
--    Adjoint(ObjA,ObjB,Left,Right)
--
--+++
--+++  Free construction via a forgetful functor.  This is an adjoint with
--+++  conventional renaming.
--+++
--define FreeConstruction(ObjA:Category,ObjB:Category):Category == with
--    Free:   ObjA -> ObjB
--    Free:   (X:ObjA,Y:ObjA,X->Y) -> (Free X -> Free Y)
--    Forget: ObjB -> ObjA 
--    Forget: (X:ObjB,Y:ObjB,X->Y) -> (Forget X -> Forget Y)
--    Adjoint(ObjA,ObjB,Free,Forget)
--    default
--        Free  (X:Domain,Y:Domain,f:X->Y):(Free X->Free Y) == left(X,Y,f)
--        Forget(X:Set,Y:Set,f:X->Y):(Forget X->Forget Y) == right(X,Y,f)
define Arrow(Obj:Category):Category == with 
    domain:    Obj
    codomain:  Obj
    arrow:  domain -> codomain
    put:      (domain,codomain) -> %
    get: % -> (domain,codomain) 
Arrow(Obj:Category,A:Obj,B:Obj,f:A->B):Arrow Obj with Set == add 
    domain:   Obj == A
    codomain: Obj == B
    arrow: domain -> codomain == (x:domain):codomain +-> ( f (x pretend A) ) pretend codomain
    Rep == domain; import from Rep
    (x:%)=(y:%):Boolean == 
        if domain has Set then 
            xd:domain == rep x
            yd:domain == rep y
            xd = yd
        else { error "Equality is not defined for this arrow." }
    coerce(x:%):OutputForm == 
        if domain has Set and codomain has Set then 
            import from codomain
            import from List OutputForm
            xd:domain == rep x
            hconcat [coerce(xd), message "->", coerce arrow xd]
        else { error "<< not available for this arrow" }
    put(a:domain,b:codomain):% == 
        if domain has Set and codomain has Set then 
            if not(arrow a=b) then error "An arrow square fails to commute."
        a pretend %
    get(x:%):(domain,codomain) == ( rep x , arrow rep x )
#if bugs_get_fixed
--   the code below causes runtime errors.
---
---  Given a category, the domain below supplies a new category where the
---  objects are Arrows and the morphisms are 2-morphisms.
---
ArrowCategory(Obj:Category,Cat:MathCategory Obj):MathCategory Arrow Obj with
    if Cat has     Final Obj then     Final Arrow Obj  
    if Cat has   Initial Obj then   Initial Arrow Obj
== add
    if Cat has   Final Obj then
        1:Arrow Obj == Arrow(Obj,(1$Cat),(1$Cat),(1$Cat)(1$Cat))
        1(A:Arrow Obj):(A->1) == (a:A):1 +-> (1$Cat)@Obj pretend 1
    if Cat has Initial Obj then
        0:Arrow Obj == Arrow(Obj,(0$Cat),(0$Cat),(0$Cat)(0$Cat))
        0(A:Arrow Obj):(0->A) == (z:0):A +-> never
--
-- this does also...  just try the most obvious thing and it will blow up
-- It seems to be compiler problems. (1.1.12p6)
--
--ArrowCategory(Cat:MathCategory Set with Final Set):MathCategory Arrow Set with 
--    Final Arrow Set
--== add
--    1:Arrow Set == Arrow(Set,(1$Cat),(1$Cat),(1$Cat)(1$Cat)) 
--    1(A:Arrow Set):(A->1) == (a:A):1 +-> (1$Cat)@Set pretend 1
--
#endif
define AutomorphismCategory(Obj:Category,A:Obj):Category == Groups with
    aut:     (A->A,A->A) -> %  -- create an automorphism from a morphism and it's inverse
    aut: % ->(A->A,A->A)       -- create a morphism and it's inverse from an automorphism
+++
+++  If X is an object in any category, Aut X given below is the group
+++  of automorphisms.  If the category has Set and CountablyInfinite, 
+++  autmorphisms are said to be equal if they have equal values at each
+++  point in their domain.
+++
define Automorphism(Obj:Category):Category == with
    Aut: (A:Obj) -> AutomorphismCategory (Obj,A)
    default
        Aut(A:Obj):AutomorphismCategory(Obj,A) == 
            WW0:AutomorphismCategory(Obj,A) == add
                Rep == Record(iso:A->A,isi:A->A); import from Rep
                1:% == per [(a:A):A +-> a, (a:A):A +-> a]
                (x:%)=(y:%):Boolean == 
                     A has CountablyFinite with Set => 
                         import from A
                         forall? ( ((rep x).iso)(a) = ((rep y).iso)(a) for a in (elements$A)() )
                     error "Equality is not available for these automorphisms."
                import from o(Obj,A,A,A)
                (g:%)*(f:%):% == per [ ((rep g).iso) ** ((rep f).iso) , ((rep f).isi) ** ((rep g).isi) ]
                inv(f:%):% == per [ (rep f).isi, (rep f).iso ]
                aut(isomorphism:A->A,isomorphismInverse:A->A):% == per [isomorphism,isomorphismInverse]
                aut(f:%):(A->A,A->A) == explode rep f 
                coerce(f:%):OutputForm == message "[Automorphism]"
            WW0 add
define EndomorphismCategory(Obj:Category,A:Obj):Category == Monoids with
    end:        (A->A) -> %  -- create an endomorphisms from a morphism
    end:   % -> (A->A)       -- create a morphism from an endomorphism
+++
+++  If X is an object in any category, End X given below is the monoid
+++  of endomorphisms.  If the category has Set and CountablyInfinite,
+++  endomorphisms are computed to be equal if they have equal values at
+++  each point in their domain.
+++
define Endomorphism(Obj:Category):Category == with
    End: (A:Obj) -> EndomorphismCategory(Obj,A) 
    default
        End(A:Obj):EndomorphismCategory(Obj,A) == 
            WW1:EndomorphismCategory(Obj,A) == add
                Rep ==> A->A
                1:% == per ( (a:A):A +-> a )
                import from o(Obj,A,A,A)
                (x:%)=(y:%):Boolean == 
                    A has CountablyFinite with Set => 
                        import from A
                        forall? ( (rep x) a = (rep y) a for a in (elements$A)() )
                    error "Equality is not available for endomorphisms."
                (g:%)*(f:%):% == per ( (rep g)**(rep f) )
                end(f:A->A):% == per f
                end(f:%):(A->A) == rep f
                coerce(f:%):OutputForm == message "[Endomorphism]"
            WW1 add
define Morphisms(Obj:Category):Category == Join(Automorphism Obj, Endomorphism Obj)
+++
+++  The Aldor category of mathematical categories
+++
define MathCategory(Obj:Category):Category == Join(Id Obj, Compose Obj, Morphisms Obj)
+++
+++  One sometimes needs the Hom-style categories where morphisms from A to B
+++  are objects in Hom(A,B) rather than A->B.
+++
define MathCategory(Obj:Category,Hom:(Obj,Obj)->Domains):Category == with 
    id: (A:Obj) -> Hom(A,A)
    compose: (A:Obj,B:Obj,C:Obj) -> (Hom(A,B),Hom(B,C)) -> Hom(A,C)
+++
+++  Identities
+++
define Id(Obj:Category):Category == with
    id: (A:Obj) -> (A->A)
    default
       id(A:Obj):(A->A) == (a:A):A +-> a
+++
+++  Composition of Morphisms
+++   
define Compose(Obj:Category):Category == with
    compose: (A:Obj,B:Obj,C:Obj) -> (A->B,B->C) -> (A->C)
    default
        compose(A:Obj,B:Obj,C:Obj)(f:A->B,g:B->C):(A->C) == (a:A):C +-> g f a
+++
+++  Initial Objects
+++    
define Initial(Obj:Category):Category == with
    Zero: () -> Obj
    zero: (A:Obj) -> (Zero()->A)
--    0: Obj
--    0: (A:Obj)->(0->A)
+++
+++  Final Objects
+++    
define Final(Obj:Category):Category == with
    One: () -> Obj
    one: (A:Obj) -> (A->One())
--    1: Obj
--    1: (A:Obj)->(A->1)   
+++
+++   Equalizer
+++    
define Equalizer(Obj:Category):Category == with
    Equalizer:   (A:Obj,B:Obj,A->B,A->B) -> (E:Obj,E->A)
+++
+++   CoEqualizer
+++    
define CoEqualizer(Obj:Category):Category == with
    CoEqualizer: (A:Obj,B:Obj,B->A,B->A) -> (E:Obj,A->E)
+++
+++   Pullback Square
+++    
define Pullback(Obj:Category):Category == with
    Pullback: (A:Obj,C:Obj,B:Obj) -> (A->C,B->C) -> ( Pullback:Obj, Pullback->A,Pullback->B,(X:Obj,X->A,X->B) -> (X->Pullback))
+++
+++   Pushout Square, the dual of a Pullback Square
+++    
define Pushout(Obj:Category):Category == with
    Pushout:  (A:Obj,C:Obj,B:Obj) -> (C->A,C->B) -> ( Pushout:Obj, A->Pushout,B->Pushout, (X:Obj,A->X,A->X) -> ( Pushout->X))
+++
+++   Exponential object
+++
define Exp(Obj:Category,E:Obj):Category == with
    rightProductFunctor: Obj -> Obj
    expFunctor:          Obj -> Obj
    Adjoint(Obj,Obj,rightProductFunctor,expFunctor)
define Exponential(Obj:Category):Category == with
    Exp: (E:Obj) -> Exp(Obj,E)
define Hom(Obj:Category):Category == with 
    Hom: (Obj,Obj) -> Obj
define Hom?(Obj:Category):Category == with
    hom?: (Obj,Obj) -> Boolean  -- hom?(A,B) answers "Are there any Homs from A to B?"
+++
+++   Decategorification
+++
define Isomorphic(Obj:Category):Category == with
    isomorphic?: (A:Obj,B:Obj) -> Boolean
    Decategorify: Set with { object: Obj -> % }
    default
        Decategorify: Set with { object: Obj -> % } == add
            Rep == Obj
            object(A:Obj):% == per A
            (A:%)=(B:%):Boolean == isomorphic? ( rep A, rep B)
            coerce(A:%):OutputForm == message "[Object]"
+++
+++  Cartesian Closed Categories
+++
define CartesianClosedCategory(Obj:Category):Category == MathCategory Obj with _
                                                              Product Obj with _
                                                          Exponential Obj 
+++
+++  Direct Product of objects and morphisms
+++     
define Product(Obj:Category):Category == with
    Product: (A:Obj,B:Obj) -> ( AB:Obj, AB->A, AB->B, (X:Obj)->(X->A,X->B)->(X->AB) )
    Product: (A1:Obj,B1:Obj,  A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
    *:(Obj,Obj)-> with Obj
    default
        Product(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2)) ==
            (ab1:Obj,pa1:ab1->A1,pb1:ab1->B1, product1: (X:Obj) -> (X->A1,X->B1) -> (X->ab1)) == Product(A1,B1)
            (ab2:Obj,pa2:ab2->A2,pb2:ab2->B2, product2: (X:Obj) -> (X->A2,X->B2) -> (X->ab2)) == Product(A2,B2)
            (f:A1->A2)*(g:B1->B2):(ab1->ab2) == product2 ( ab1 )( (x:ab1):A2 +-> f pa1 x, (x:ab1):B2 +-> g pb1 x )
            (ab1,ab2,*)
        (A:Obj)*(B:Obj): with Obj == 
            (AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB)) == Product(A,B)
            AB add
+++
+++  Direct Sum
+++
define CoProduct(Obj:Category):Category == with
    CoProduct: (A:Obj,B:Obj) -> ( AB:Obj, A->AB, B->AB, (X:Obj)->(A->X,B->X)->(AB->X) )
    CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) -> (AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
    +:(Obj,Obj)-> with Obj
    default
        CoProduct(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1)) == 
            (ab1:Obj,ia1:A1->ab1,ib1:B1->ab1, sum1: (X:Obj) -> (A1->X,B1->X) -> (ab1->X)) == CoProduct(A1,B1)
            (ab2:Obj,ia2:A2->ab2,ib2:B2->ab2, sum2: (X:Obj) -> (A2->X,B2->X) -> (ab2->X)) == CoProduct(A2,B2)
            (f:A2->A1)+(g:B2->B1):(ab2->ab1) == sum2 ( ab1 ) ( (x:A2):ab1 +-> ia1 f x, (x:B2):ab1 +-> ib1 g x )
            (ab1,ab2,+)
        (A:Obj)+(B:Obj): with Obj == 
            (AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X)) == CoProduct(A,B)
            AB add
+++
+++  Multiple Direct Product of a Single Object
+++    
define MultiProduct(Obj:Category):Category == with
    Product:(A:Obj,n:Integer)   -> (Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
    ^:(Obj,Integer) -> with Obj
    default
        (A:Obj)^(n:Integer): with Obj ==
            (Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple (X->A))->(X->Prod)) == Product(A,n)
            Prod add
+++
+++  Multiple Direct Sum of a Single Object
+++         
define CoMultiProduct(Obj:Category):Category == with
    CoProduct:(A:Obj,n:Integer) -> ( Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
    ..:(Obj,Integer) -> with Obj
    default
        (A:Obj)..(n:Integer): with Obj == 
            (Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple (A->X))->(Sum->X)) == CoProduct(A,n)
            Sum add
+++
+++  Quotients
+++ 
define Quotient(Obj:Category):Category == with
    Quotient:  (A:Obj,B:Obj) -> (A->B) -> (Quo:Obj,A->Quo,(X:Obj)->(A->X)->(Quo->X))
    /:(A:Obj,B:Obj) -> ((A->B)->Obj)
    default
        (A:Obj)/(B:Obj):((A->B)->Obj) ==
            F(f:A->B):Obj == 
                (Q:Obj,insert:A->Q,quo:(X:Obj)->(A->X)->(Q->X)) == Quotient(A,B)(f)
                Q add
            F
+++
+++   Subobjects (the dual of Quotients)
+++    
define Subobject(Obj:Category):Category == with
    Subobject: (A:Obj,B:Obj) -> (B->A) -> (Sub:Obj,Sub->A,(X:Obj)->(X->A)->(X->Sub))
    \:(A:Obj,B:Obj) -> ((B->A)->Obj)
    default
        (A:Obj)\(B:Obj):(B->A)->Obj ==
            F(f:(B->A)): Obj ==
                (S:Obj,include:S->A,sub:(X:Obj)->(X->A)->(X->S)) == Subobject(A,B)(f)
                S add
            F

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/categories.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 ./categories.lsp
   Issuing )library command for categories
   Reading /var/zope2/var/LatexWiki/categories.asy
   Final is now explicitly exposed in frame initial 
   Final will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Initial is now explicitly exposed in frame initial 
   Initial will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Arrow is now explicitly exposed in frame initial 
   Arrow will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   FreeConstruction is now explicitly exposed in frame initial 
   FreeConstruction will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   LeftAdjoint is now explicitly exposed in frame initial 
   LeftAdjoint will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   CartesianClosedCategory is now explicitly exposed in frame initial 
   CartesianClosedCategory will be automatically loaded when needed 
      from /var/zope2/var/LatexWiki/categories
   RightAdjoint is now explicitly exposed in frame initial 
   RightAdjoint will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   MathCategory is now explicitly exposed in frame initial 
   MathCategory will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Exponential is now explicitly exposed in frame initial 
   Exponential will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Id is now explicitly exposed in frame initial 
   Id will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Compose is now explicitly exposed in frame initial 
   Compose will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Morphisms is now explicitly exposed in frame initial 
   Morphisms will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   AutomorphismCategory is now explicitly exposed in frame initial 
   AutomorphismCategory will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Automorphism is now explicitly exposed in frame initial 
   Automorphism will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Product is now explicitly exposed in frame initial 
   Product will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Subobject is now explicitly exposed in frame initial 
   Subobject will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Exp is now explicitly exposed in frame initial 
   Exp will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Quotient is now explicitly exposed in frame initial 
   Quotient will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Endomorphism is now explicitly exposed in frame initial 
   Endomorphism will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   CoMultiProduct is now explicitly exposed in frame initial 
   CoMultiProduct will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   EndomorphismCategory is now explicitly exposed in frame initial 
   EndomorphismCategory will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   CoProduct is now explicitly exposed in frame initial 
   CoProduct will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   MultiProduct is now explicitly exposed in frame initial 
   MultiProduct will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Adjoint is now explicitly exposed in frame initial 
   Adjoint will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Isomorphic is now explicitly exposed in frame initial 
   Isomorphic will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Hom? is now explicitly exposed in frame initial 
   Hom? will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Hom is now explicitly exposed in frame initial 
   Hom will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Pushout is now explicitly exposed in frame initial 
   Pushout will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Pullback is now explicitly exposed in frame initial 
   Pullback will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   CoEqualizer is now explicitly exposed in frame initial 
   CoEqualizer will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories
   Equalizer is now explicitly exposed in frame initial 
   Equalizer will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/categories