[Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product.

[Gabriel Dos Reis]

On Mon, 22 Oct 2007, Bill Page wrote:

| Yes, that is the point. Apparently Stephen Watt's answer in Aldor is
| that allow the domain of 'Domain' to be 'Domain' is ok provided we are
| careful exactly what operations we expect to provide in 'Domain'.

Domain:Domain introduces an inconsistency at its Curry-Howard logic
level, so I'm nervous about that.  A solution, adopted by Coq, is that
even though the interface would display Type:Type, what it really does
it that it has an infinite hierarchy of universes Type(k), where 
Type(i) : Type(j), for i < j, starting from 0.

-- Gaby