`{Univalence} (g : Type <~> Type) (ge : g Empty <> Empty) : ~~ExcludedMiddle_type. Proof. pose (f := equiv_inverse g). intros nlem. apply ge. apply path_universe_uncurried, equiv_to_empty; intros gz. apply nlem. apply (lem_from_aut_type_inhabited_empty f (g Empty) (tr gz)). unfold f; apply eissect. Defined.
Require Import Basics Types. Require Import HoTT.Truncations. Require Import Universes.BAut Universes.Rigid. Require Import ExcludedMiddle.