Definition invezmaphf {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) : hfiber f (pr1 ye). Proof. intros. split with (pr1 (pr1 xee')). apply (maponpaths (hfiberpr1 _ _) (pr2 xee')). Defined.