Definition hfp_right {X Y Z : UU} (f : X -> Z) (g : Y -> Z) : hfp f g ≃ ∑ y, hfiber f (g y). Proof. intros. use weq_iso. - intros [[x y] e]. exact (y,,x,,!e). - intros [x [y e]]. exact ((y,,x),,!e). - intros [[x y] e]. apply maponpaths, pathsinv0inv0. - intros [x [y e]]. apply maponpaths, maponpaths, pathsinv0inv0. Defined.