Edit detail for SandBox Aldor Category Theory 3 revision 2 of 7

aldor
#include "axiom"
#pile
#library    lBasics  "basics.ao"
import from lBasics
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