Definition homotffggid {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) : (ffgg f g z ye xee') = xee'. Proof. intros. induction ye as [ y e ]. induction e. induction xee' as [ xe e' ]. induction e'. induction xe as [ x e ]. induction e. simpl. apply idpath. Defined.