{A : Type} {P : A -> Type} `{forall x, IsHProp (P x)} {a b : A} (p : a = b) (x : P a) (y : P b) : path_sigma_hprop (b;y) (a;x) p^ = (path_sigma_hprop (a;x) (b;y) p)^. Proof. destruct p; simpl. rewrite (path_ishprop x y). refine (path_sigma_hprop_1 _ @ (ap inverse (path_sigma_hprop_1 _))^). Qed.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.