Corollary isofhlevelfhomot2 (n : nat) {X X' Y : UU} (f : X -> Y) (f' : X' -> Y) (w : X ≃ X') (h : ∏ x : X, paths (f x) (f' (w x))) : isofhlevelf n f -> isofhlevelf n f'. Proof. intros X0. assert (X1 : isofhlevelf n (λ x : X, f' (w x))) by apply (isofhlevelfhomot n _ _ h X0). apply (isofhlevelfgwtog n w f' X1). Defined.