[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures
From: 
Ralf Hemmecke 
Subject: 
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures 
Date: 
Tue, 14 Mar 2006 18:30:11 +0100 
Useragent: 
Thunderbird 1.5 (X11/20051201) 
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 elementof relation. I.e.
the Aldor category 'Monoid(Integer,*,1)' is a subcategory
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
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, (continued)
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/04
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/04
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/14
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures,
Ralf Hemmecke <=
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/14
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/14