Theorem isofhlevelffromXY (n : nat) {X Y : UU} (f : X -> Y) : isofhlevel n X -> isofhlevel (S n) Y -> isofhlevelf n f. Proof. revert X Y f. induction n as [ | n IHn ]. - intros X Y f X0 X1. assert (is1 : isofhlevel O Y). { split with (f (pr1 X0)). intro t. unfold isofhlevel in X1. set (is := X1 t (f (pr1 X0))). apply (pr1 is). } apply (isweqcontrcontr f X0 is1). - intros X Y f X0 X1. unfold isofhlevelf. simpl. assert (is1 : ∏ x' x : X, isofhlevel n (x' = x)) by (simpl in X0; assumption). assert (is2 : ∏ y' y : Y, isofhlevel (S n) (y' = y)) by (simpl in X1; simpl; assumption). assert (is3 : ∏ (y : Y) (x : X) (xe' : hfiber f y), isofhlevelf n (d2g f x xe')) by (intros; apply (IHn _ _ (d2g f x xe') (is1 (pr1 xe') x) (is2 (f x) y))). assert (is4 : ∏ (y : Y) (x : X) (xe' : hfiber f y) (e : (f x) = y), isofhlevel n ((make_hfiber f x e) = xe')) by (intros; apply (isofhlevelweqb n (ezweq3g f x xe' e) (is3 y x xe' e))). intros y xe xe'. induction xe as [ t x ]. apply (is4 y t xe' x). Defined.