equiv_swap_types <> equiv_idmap. Proof. intros p. assert (q := equiv_swap_types_swaps). strip_truncations. apply ne. apply equiv_path. rewrite p in q; exact q. Qed.
Require Import Basics Types. Require Import HoTT.Truncations. Require Import Universes.BAut Universes.Rigid. Require Import ExcludedMiddle.