The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Sep 10, 2012 at 5:20 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> So this means that any inductive type with more than one constructor lives
> in at least [Set]?

Right, or an inductive type with one constructor but where the
constructor has data arguments (but in that case, it's probably taken
care of implicitly without the need to add a Set explicitly in the
universe level).  Probably exactly the cases where it wouldn't
generate a *_rect if you forced it into Prop, but don't quote me on
that.

> I'm still confused, though.  I get the following in coqtop
>
> Set Printing Universes.
> Inductive sumT (A B : Type) :=
> | inlT : A -> sumT A B
> | inrT : B -> sumT A B.
> Inductive sumP (A B : Type) : Prop :=
> | inlP : A -> sumP A B
> | inrP : B -> sumP A B.
> Check sumT.
> (* sumT
>      : Type (* Top.77 *) ->
>        Type (* Top.78 *) -> Type (* max(Set, Top.77, Top.78) *)
> *)
> Check sumP.
> (* sumP
>      : Type (* Top.91 *) -> Type (* Top.92 *) -> Prop
> *)
>
> My intuition says that if something can be forced to be in [Prop], the
> type-checker shouldn't infer it to necessarily be higher?

If you force the inductive to be in Prop, that's roughly equivalent to
taking the non-forced version and applying "inhabited", which is the
universal "forcer into Prop".  So in your example, sumP A B is
equivalent to inhabited(sumT A B) <-> inhabited A \/ inhabited B.
-- 
Daniel Schepler