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