"Bill Page" <[EMAIL PROTECTED]> writes: | On Fri, Jul 4, 2008 at 2:18 PM, Gabriel Dos Reis wrote: | > ... | > Bill Page writes: | > | I agree that just giving Type a domain definition is not a solution. I | > | think the solution to the problem has to do with defining more | > | precisely what is a "category" (i.e. in the case of Aldor a categories | > | are subtypes of Type, domains are objects of Type and therefore via | > | the subtype relation domains are also objects of categories). | > | > Depending on ones notion of `subtype', it is already the case that | > a category is a subtype of Type -- if by x is subtype of Type one | > means that the query | > | > x has Type | > | > is well formed and yields true. | | But | | Integer has Type | | is well-formed and yields true. Does that mean that Integer is a | subtype of Type,
Yes. | i.e. a category? Is your definition that a `subtype of Type is a category'? | Of course not! `not!' to which part exactly? | 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. -- Gaby ------------------------------------------------------------------------- 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