The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

So this means that any inductive type with more than one constructor lives in at least [Set]?

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?

-Jason

On Mon, Sep 10, 2012 at 1:21 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

On Mon, Sep 10, 2012 at 9:43 AM, Jason Gross <jasongross9 AT gmail.com> wrote:
> Hi,
> Can someone explain to me why the type of [sum] is
>       [Type (* Coq.Init.Datatypes.33 *) ->
>        Type (* Coq.Init.Datatypes.34 *) ->
>        Type (* max(Set, Coq.Init.Datatypes.33, Coq.Init.Datatypes.34) *)]
> In particular, why is the [sum] of two propositions in [Set], rather than in
> [Prop]?

Because from the sum P+Q, you can extract some information (which
branch an element comes from), which would be illegal for the
disjunction proposition P\/Q.  P+Q is equivalent to the type {P} + {Q}
=def= sumbool P Q, which is the more usual one to use for Props.
--
Daniel Schepler