equiv_sum_symm@{u v k | u <= k, v <= k} (A : Type@{u}) (B : Type@{v}) : Equiv@{k k} (A + B) (B + A). Proof. apply (equiv_adjointify (fun ab => match ab with inl a => inr a | inr b => inl b end) (fun ab => match ab with inl a => inr a | inr b => inl b end)); intros [?|?]; exact idpath. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.