The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Such an axiom certainly breaks extraction, since it has no natural 
computational interpretation, but perhaps you don't care about 
extraction.  It also makes Gallina "computation" highly 
non-computational, which also might not bother you, depending on the 
application.  I don't know if it's logically consistent.

On 07/02/2013 03:38 PM, Chris Casinghino wrote:
> 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).
>