Definition ezmaphf {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (ye : hfiber g z) (xe : hfiber f (pr1 ye)) : hfiber (hfibersgftog f g z) ye. Proof. intros. split with (hfibersftogf f g z ye xe). simpl. apply (hfibertriangle2 g (make_hfiber g (f (pr1 xe)) (pathscomp0 (maponpaths g (pr2 xe)) (pr2 ye))) ye (pr2 xe)). simpl. apply idpath. Defined.