The Coq mailing list

[Andrew Cave <acave1 AT cs.mcgill.ca>]

Also you may want to note that it's inconsistent if you happen to be
using -impredicative-set for some reason.

This is explained in part 2.5 of
http://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html

On Tue, Jul 2, 2013 at 3:38 PM, Chris Casinghino
<chris.casinghino AT gmail.com>
 wrote:
> Hi all,
>
> I notice that, where the Coq FAQ discusses safe axioms, it mentions
> excluded middle only for "Prop".  This also seems to be the case in
> the standard libraries.
>
> Would it also be safe to add excluded middle for "Type"?  That is,
> could I add the following?
>
> Inductive sum (A B : Type) : Type :=
>   | leftT : A -> sum A B
>   | rightT : B -> sum A B.
>
> Axiom em_type : forall A : Type, sum A (A -> False).
>
> Thanks!
>
> --Chris Casinghino