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

[Ralf Hemmecke]

On 03/14/2006 05:28 PM, Page, Bill wrote:
> 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.

OK. Monoid is a category, but I must be able to tell whether something 
is an object of that category. I never said that Ob(Monoid) is a set. I 
did not even claim that it is a class. My "\in" notation just tried to 
be "intuitive". I know that some people found mathematics on category 
theory an not set theory.

> They prefer to posit the existence of a functor.

Could you be more precise?

> 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).

He? If you say "Monoid(Integer,*,1)" is "the particular object in 
Monoid" then why would I have to write

  Integer has Monoid(Integer, *, 1) ?

That also looks unnatural. What would be the meaning of "has" and what 
should be the types of its first and second argument?

> Then the functor F maps
> Integer into Monoid(Integer,*,1):
>
>     Integer |-> Monoid(Integer,*,1)

It's hard to follow you. Let me tell you what I understood.

1) There is a category Monoid whose objects are categories. (In that 
sense Monoid would be on the same type level as "Category" in Aldor.) I 
order to avoid confusion, lets call it MONOID.

2) Monoid(Integer, *, 1) would be a category.
  I hope you _don't_ mean the category structure that comes from
  the fact that any monoid can be considered as a category.
  But than I cannot interpret what the objects and arrows in that
  category would be.

3) For me "Monoid(Integer,*,1)" looks more like the universal algebra 
given by the carrier set {0,1,-1,...} and operations * and 1 together 
with the monoid axioms. The axioms are hidden in your notation by the 
"tag" or predicate (well, it's not a predicate since you want the result 
type to be a category) "Monoid".

4) If "Monoid(Integer,*,1)" just means: take the (aldor) category that 
Integer is currently in and forget anything except * and 1, than that 
looks similar to one of my previous mails where I tried to model F by 
"MonoidStructure". It is only that I work on the left hand side of "has" 
and you on the right hand side. But also my suggestion would be "type 
satisfaction in the sense of Aldor" (if it worked).

> 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.

What would be different to

  Integer has with {*:(%,%)->%;1:%}

?? Only that "Monoid" appears?

Ralf