The Coq mailing list

[Chris Casinghino <chris.casinghino AT gmail.com>]

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