Theorem isofhlevelXfromg (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (fs : fibseqstr f g z) : isofhlevelf n g -> isofhlevel n X. Proof. intros isf. assert (w : X ≃ (hfiber g z)). apply (make_weq _ (pr2 fs)). apply (isofhlevelweqb n w (isf z)). Defined.