Theorem isofhlevelff (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) : isofhlevelf n (λ x : X, g (f x)) -> isofhlevelf (S n) g -> isofhlevelf n f. Proof. intros X0 X1. unfold isofhlevelf. intro y. set (ye := make_hfiber g y (idpath (g y))). apply (isofhlevelweqb n ( ezweqhf f g (g y) ye) (isofhlevelffromXY n _ (X0 (g y)) (X1 (g y)) ye)). Defined.