Theorem isofhlevelfffromZ (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (fs : fibseqstr f g z) (isz : isofhlevel (S n) Z) : isofhlevelf n f. Proof. intros. intro y. assert (w : (hfiber f y) ≃ ((g y) = z)). apply (invweq (ezweq1 f g z fs y)). apply (isofhlevelweqb n w (isz (g y) z)). Defined.