[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


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:


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.

Bill Page.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]