On Fri, Jul 4, 2008 at 6:32 PM, Gabriel Dos Reis wrote: > Bill Page writes: > ... > | But > | > | Integer has Type > | > | is well-formed and yields true. Does that mean that Integer is a > | subtype of Type, > > Yes. >
Ok, I will consider this. I would have said (with Stephen Watt and Aldor) that Integer is a Domain-valued object (an object of the domain Domain). But you have domains as subtypes of the category Type. Therefore everything besides objects are subtypes of Type? > | i.e. a category? > > Is your definition that a `subtype of Type is a category'? > I considered that since Type is a category that it's subtypes would also be categories, but I guess that is an unjustified assumption. > | Of course not! > > `not!' to which part exactly? > I withdraw my exclamation. > | Axiom has two different uses of 'has'. One of them represents the subtype > | (inclusion) relation, the other is the membership relation. > > Now, I have two undefined terms (subtype and inclusion) precisely when > I'm trying to get you define just one (subtype). We are not progressing. > You are right. I fear that I have reached the limit of my cognition at this point and it might be best to let this subject rest again for awhile... Thanks. Regards, Bill Page. ------------------------------------------------------------------------- Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW! Studies have shown that voting for your favorite open source project, along with a healthy diet, reduces your potential for chronic lameness and boredom. Vote Now at http://www.sourceforge.net/community/cca08 _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
