Corollary iscontrhfiberii1x (X Y : UU) (x : X) : iscontr (hfiber (@ii1 X Y) (ii1 x)). Proof. intros. set (xe1 := make_hfiber (@ii1 _ _) x (idpath (@ii1 X Y x))). apply (iscontraprop1 (isinclii1 X Y (ii1 x)) xe1). Defined.