fact: Definition equiv_swap_empty_unit `{Univalence} `{ExcludedMiddle} : Type <~> Type := equiv_swap_rigid Empty Unit (fun e => e^-1 tt).
imports: Basics Types HoTT.Truncations Spaces.BAut Spaces.BAut.Rigid ExcludedMiddle