∀ {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} {δ : Sort u_4} (e₁ : α ≃ β) (e₂ : γ ≃ δ),
  Function.RightInverse (fun x => PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) fun x =>
    PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)