`{Funext} : DNE_type -> ExcludedMiddle_type. Proof. intros dn P hp. refine (dn (P + ~P) _ _). - apply ishprop_sum. + exact _. + exact _. + intros p np; exact (np p). - intros nlem. apply nlem. apply inr. intros p. apply nlem. apply inl. apply p. Defined.
Require Import HoTT.Basics HoTT.Types.