axiom-developer
[Top][All Lists]

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

 From: Page, Bill Subject: RE: [Axiom-developer] Curiosities with Axiom mathematical structures Date: Tue, 14 Mar 2006 11:28:46 -0500

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.