Ralf,
On Tuesday, March 14, 2006 9:56 AM you wrote:
>
> On 03/14/2006 01:43 AM, Gabriel Dos Reis wrote:
> > "Bill Page" <[EMAIL PROTECTED]> 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.
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
