Definition hfibersgtof' {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 (h z) (maponpaths f e)). Defined.