Theorem isofhlevelfgf (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) : isofhlevelf n f -> isofhlevelf n g -> isofhlevelf n (λ x : X, g (f x)). Proof. intros X0 X1. unfold isofhlevelf. intro z. assert (is1 : isofhlevelf n (hfibersgftog f g z)). { unfold isofhlevelf. intro ye. apply (isofhlevelweqf n (ezweqhf f g z ye) (X0 (pr1 ye))). } assert (is2 : isofhlevel n (hfiber g z)) by apply (X1 z). apply (isofhlevelXfromfY n _ is1 is2). Defined.