`{Univalence} `{ExcludedMiddle} : Type <~> Type := equiv_swap_rigid Empty Unit (fun e => e^-1 tt).
Require Import Basics Types. Require Import HoTT.Truncations. Require Import Universes.BAut Universes.Rigid. Require Import ExcludedMiddle.