Edit detail for SandBox Aldor Category Theory 4 revision 5 of 5

#include "axiom"
#pile
#library    lBasics  "basics.ao"
import from lBasics

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 == Automorphism Obj with Endomorphism Obj

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/morphisms.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.
   The )library system command was not called after compilation.

)library basics.ao

Reading /var/aw/var/LatexWiki/basics.asy
   Domain is now explicitly exposed in frame initial 
   Domain will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Set is now explicitly exposed in frame initial 
   Set will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Printable is now explicitly exposed in frame initial 
   Printable will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Preorder is now explicitly exposed in frame initial 
   Preorder will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   TotalOrder is now explicitly exposed in frame initial 
   TotalOrder will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   associativeProduct is now explicitly exposed in frame initial 
   associativeProduct will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Countable is now explicitly exposed in frame initial 
   Countable will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   CountablyFinite is now explicitly exposed in frame initial 
   CountablyFinite will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Monoids is now explicitly exposed in frame initial 
   Monoids will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Groups is now explicitly exposed in frame initial 
   Groups will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   MapCategory is now explicitly exposed in frame initial 
   MapCategory will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Map is now explicitly exposed in frame initial 
   Map will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   Categorify is now explicitly exposed in frame initial 
   Categorify will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   null is now explicitly exposed in frame initial 
   null will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics
   o is now explicitly exposed in frame initial 
   o will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/basics

)show Domains

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

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