[Aldor-l] [open-axiom-devel] [#428] 'Domain' in 'SetCategory'?

[Ralf Hemmecke]

>> For me 'Category' and 'Type' are somewhat special.
>> Let me define as Saul Youssef did in Section 2 of
>> http://axiom-portal.newsynthesis.org/refs/articles/Youssef-ProspectsForCategoryTheoryInAldor.pdf
>>
>>  Domain: Category == with;
>>
> 
> I don't have any problems with defining a category of this sort for
> specific purposes. In fact such categories are called "properties" in
> all flavors of Axiom.
> 
>> then I would (roughly) say that
>>
>>  Type = Category + Domain + {Type}
>>
>> i.e. Type comprises all categories, all domains and itself. The constant
>> 'Category' (which is a keyword) is on the same level as 'Type' but with
>> less inhabitants than 'Type'.
>>
> 
> I don't like this much since it seem to conflict with the actual usage
> of these terms in both Axiom and Alsor.

Why do you see a conflict here? Is, what I say, not what Doye says in
Section 2.5 of 
http://axiom-portal.newsynthesis.org/refs/articles/doye-aldor-phd.pdf/?searchterm=doye
?

items \in Domains \in Categories \in Category

where in my notation above "Domain" should just be considered the top of 
the category hierarchy. (Actually, the top is "with", I just named it 
"Domain").

Is OpenAxiom going to somehow blur the distinction between categories 
and domains?

I understand that it would be nice to really use categories as first 
class objects, but that does not mean that they must be considered as 
domains. Or does it?

Does http://axiom-portal.newsynthesis.org/refs/articles/define.pdf have 
something to do with your discussion?

Ralf