`{Univalence} `{ExcludedMiddle} (A B : Type) `{IsRigid A} `{IsRigid B} (ne : ~(A <~> B)) : Type <~> Type. Proof. refine (equiv_swap_types A B ne _). apply equiv_contr_contr. Defined.
Require Import Basics Types. Require Import HoTT.Truncations. Require Import Universes.BAut Universes.Rigid. Require Import ExcludedMiddle.