proposition: Theorem isofhlevelfhomot (n : nat) {X Y : UU} (f f' : X -> Y) (h : ∏ x : X, paths (f x) (f' x)) : isofhlevelf n f -> isofhlevelf n f'.
proof: Proof. intros X0. unfold isofhlevelf. intro y. apply (isofhlevelweqf n (weqhfibershomot f f' h y) (X0 y)). Defined.
imports: UniMath.Foundations.PartA