Lemma iscontrhfiberofincl {X Y : UU} (f : X -> Y) : isincl f -> (∏ x : X, iscontr (hfiber f (f x))). Proof. intros X0 x. unfold isofhlevelf in X0. set (isy := X0 (f x)). apply (iscontraprop1 isy (make_hfiber f _ (idpath (f x)))). Defined.