Theorem isofhlevelfgtogw (n : nat) {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z) (is : isofhlevelf n g) : isofhlevelf n (λ x : X, g (w x)). Proof. intros. intro z. assert (is' : isweq (hfibersgftog w g z)). { intro ye. apply (iscontrweqf (ezweqhf w g z ye) (pr2 w (pr1 ye))). } apply (isofhlevelweqb _ (make_weq _ is') (is _)). Defined.