The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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