Definition hfibersg'tof {X X' Y Z : UU} (f : X -> Y) (f' : X' -> Y) (g : Z -> X) (g' : Z -> X') (h : commsqstr g' f' g f) (x' : X') (ze : hfiber g' x') : hfiber f (f' x'). Proof. intros. induction ze as [ z e ]. split with (g z). apply (pathscomp0 (pathsinv0 (h z)) (maponpaths f' e)). Defined.