RE: [Axiom-developer] Curiosities with Axiom mathematical structures

[Page, Bill]

Ralf, 

On Tuesday, March 14, 2006 9:56 AM you wrote:
> 
> On 03/14/2006 01:43 AM, Gabriel Dos Reis wrote:
> > "Bill Page" <address@hidden> writes:
> > 
> > | I agree with Martin. One should interpret:
> > | 
> > |   if Integer has Monoid(*,1)
> > | 
> > | as the question of whether F = (*,1) is a functor from 
> > | the category containing Integer to Monoid, the category
> > | of monoids.
> > 
> > 100% agreed.
> 
> But that looks like strange syntax to me. If I want to ask
> 
>    F(Integer) \in Ob(Monoid)
> 
> and I have to write "Integer has Monoid(*,1)" that does not 
> really look natural to me.
> 

Category theorists purist do not like to write set membership
because it implies that categories are always sets. They
prefer to posit the existence of a functor. But you are right,
describing the functor this way does not seem very "natural"
in Aldor syntax.

What if we say:

  Monoid(Integer,*,1)

denotes the particular object in Monoid (since this is what
we have to write in Aldor anyway). Then the functor F maps
Integer into Monoid(Integer,*,1):

    Integer |-> Monoid(Integer,*,1)

The objects in Monoid are categories both in the sense of
Aldor and in the sense of category theory. Then:

  Integer has Monoid(Integer,*,1)

Looks "natural" since this depends a the Aldor category
containment relation rather than an element-of relation. I.e.
the Aldor category 'Monoid(Integer,*,1)' is a sub-category
of the Aldor category containing Integer. This is just the
concept of type satisfaction in Aldor.

Regards,
Bill Page.