Corollary weqhfibersgwtog {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z) (z : Z) : hfiber (funcomp w g) z ≃ hfiber g z. Proof. intros. split with (hfibersgftog w g z). intro ye. apply (iscontrweqf (ezweqhf w g z ye) ((pr2 w) (pr1 ye))). Defined.