Re: [Axiom-developer] A curious algebra failure

[Stephen Wilson]

Gabriel Dos Reis <address@hidden> writes:

> On Sat, 11 Aug 2007, Stephen Wilson wrote:
> 
> | Gabriel Dos Reis <address@hidden> writes:
> | > | Here, % certainly satisfies the conditions on the parameter type:
> | > | 
> | > |    SetCategory with "*": (%,%)->%
> | > 
> | > I don't think it does, in the sense of Spad.
> | > I believe two unnamed categories define distinct categories irrespective 
> of
> | > their bodies. 
> | 
> | Are you saying that % is unnamed?
> 
> `%' is not a category; it stands for the current domain.
> 
> I'm saying that the category
> 
>     SetCategory with "*": (%,%)->%
> 
> is unnamed.

Right.  What I am saying is that in the type context

    S : SetCategory with "*": (%, %) -> %

when % denotes MONAD, the category of % (its `principle category' as I
called it, since in the general case it is anonymous), satisfies the
context.  Certainly MONAD has SetCategory and an export "*": (%, %) ->
%.  The nominal/structural typing rules (not that I have tried to
define them formally) are just my way of thinking about the issue.

If this interpretation does not hold, what kind of expression could
possibly satisfy the context S above?
 
> I'm trying to find where I found that in the Axiom book, but no luck for the
> moment.  Except the discussion in section 12.12 on Anonymous Categories.

As I said, I do not recall reading anything explicit on this point,
but I would be grateful if you can pull up a reference.  I might take
a look in the Aldor user guide and see if there is mention there.


Steve