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