"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.
| Axiom/Aldor language constraints require us to write
|
| Integer has Monoid(Integer,*,1)
|
| Martin has suggested a method using 'extend' in Aldor to make
| such an assertion by:
|
| extend Integer: Monoid(Integer,+,1)
all that makes sense, except that -- upon reflection this a while --
not everythign should be explicit parameter.
Basically, the idea is this. When have (T, op, e) as a monoid, it is
because the three elements together satisfy some relations. If I may
borrow some loose analogy, it is like with implicit functions. The
above means that there are some redundancy in the triple. Here, e is
uniquely defined by op (maybe non-constructively, but when it exists
it is unique). Consequently the neutral element is a function of op
and T. So I would write
Inetger has Monoid(Integer, *)
extend Integer: Monoid(Integer, +) with {
neutral == 0;
}
-- Gaby
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
