Definition ffgg {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) : hfiber (hfibersgftog f g z) ye. Proof. intros. induction ye as [ y e ]. induction e. unfold hfibersgftog. unfold hfibersgftog in xee'. induction xee' as [ xe e' ]. induction xe as [ x e ]. set (e'' := (maponpaths g (maponpaths (hfiberpr1 g (g y)) e'))). simpl in e'. split with (make_hfiber (funcomp f g) x (pathscomp0 e'' (idpath (g y)))). simpl. apply (hfibertriangle2 _ (make_hfiber g (f x) (pathscomp0 e'' (idpath (g y)))) (make_hfiber g y (idpath _)) (maponpaths (hfiberpr1 _ _) e') (idpath _)). Defined.