equiv_sigma_assoc' `(P : A -> Type) (Q : forall a : A, P a -> Type) : {a : A & {p : P a & Q a p}} <~> {ap : sig P & Q ap.1 ap.2}. Proof. make_equiv. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.