equiv_sigma_symm' {A : Type} `(P : A -> Type) `(Q : A -> Type) : { ap : { a : A & P a } & Q ap.1 } <~> { aq : { a : A & Q a } & P aq.1 }. Proof. make_equiv. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.