The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

On 02/05/2011 09:17, Gert Smolka wrote:
> 1. Why does Coq ignore my wish to place the types
> in one of the universes Type ranges over?
> 
> 2. Why are zero and one put into Prop while
> two is put into Set?

As far as I know, Coq chooses the minimal universe for your inductive
types. The difference between zero/one and two comes from the «
no-flow-from-Prop-to-Type principle ».

Indeed, zero and one have respectively zero and one with arguments in
Prop constructors, so they can be put in the minimal universe Prop
without any loss of expressivity. Meanwhile, two shall be put in the
minimal universe in Type, that is Set, to keep the disjunction properties.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature