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 _______________________________________________ Axiom-math mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-math
