Corollary iscontrhfiberii2y (X Y : UU) (y : Y) : iscontr (hfiber (@ii2 X Y) (ii2 y)). Proof. intros. set (xe1 := make_hfiber (@ii2 _ _) y (idpath (@ii2 X Y y))). apply (iscontraprop1 (isinclii2 X Y (ii2 y)) xe1). Defined.