Theorem isofhlevelXfromfY (n : nat) {X Y : UU} (f : X -> Y) : isofhlevelf n f -> isofhlevel n Y -> isofhlevel n X. Proof. revert X Y f. induction n as [ | n IHn ]. - intros X Y f X0 X1. apply (iscontrweqb (make_weq f X0) X1). - intros X Y f X0 X1. simpl. assert (is1 : ∏ (y : Y) (xe xe': hfiber f y), isofhlevel n (xe = xe')) by (intros; apply (X0 y)). assert (is2 : ∏ (y : Y) (x : X) (xe' : hfiber f y), isofhlevelf n (d2g f x xe')). { intros. unfold isofhlevel. intro y0. apply (isofhlevelweqf n (ezweq3g f x xe' y0) (is1 y (make_hfiber f x y0) xe')). } assert (is3 : ∏ (y' y : Y), isofhlevel n (y' = y)) by (simpl in X1; assumption). intros x' x. set (y := f x'). set (e' := idpath y). set (xe' := make_hfiber f x' e'). apply (IHn _ _ (d2g f x xe') (is2 y x xe') (is3 (f x) y)). Defined.