Definition iscontr_singleton {X : hSet} (x : X) : iscontr (singleton x). Proof. use make_iscontr. - exact singleton_point. - intros t. apply subtypePath_prop. apply(squash_to_prop (pr2 t)). apply setproperty. intro ; assumption. Defined.