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