equiv_sigma_prod' `(Q : A -> B -> Type) : {a : A & {b : B & Q a b}} <~> sig (fun ab => Q (fst ab) (snd ab)). Proof. make_equiv. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.