`{Univalence} (f : Type <~> Type) (eu : f Unit = Empty) : ExcludedMiddle_type. Proof. apply DNE_to_LEM, DNE_from_allneg; intros P ?. exists (f P); split. - intros p. assert (Contr P) by (apply contr_inhabited_hprop; assumption). assert (q : Unit = P) by (apply path_universe_uncurried, equiv_contr_contr). destruct q. rewrite eu. auto. - intros nfp. assert (q : f P = Empty) by (apply path_universe_uncurried, equiv_to_empty, nfp). rewrite <- eu in q. apply ((ap f)^-1) in q. rewrite q; exact tt. Defined.
Require Import Basics Types. Require Import HoTT.Truncations. Require Import Universes.BAut Universes.Rigid. Require Import ExcludedMiddle.