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

[Ralf Hemmecke]

> | > | I think the way out of this mess was correctly identified by Stephen
> | > | Watt in the description of Aldor when he wrote: (ibid.):
> | > |
> | > | "Each domain is itself a value belonging to the domain Type. Domains
> | > | may additionally belong to some number of subtypes (of Type), known
> | > | as categories."
>> ...
>> Nothing in the semantics specification (the quote above without the
>> first sentence) requires Type to be a domain.

> I agree.

Yep.

I have no proof of it, but in my understanding Type is the type of all 
Aldor types including itself. Type lives conceptually above domains and 
categories. Maybe 'Type' is comparable to 'the class of all classes' in 
set theory (even if NBG
http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory
does not admit it).

I know it proves nothing, but have you looked at a comment in
https://svn.origo.ethz.ch/algebraist/trunk/aldor/lib/aldor/src/lang/sal_lang.as
where it says?

-- Nice idea, but rejected by the compiler
-- Type:Category == add;

(Just a funny side remark.)

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;

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'.

Forgive me if anything is wrong, I am not a language expert.

Ralf