Contractible

A type $X$ is contractible if there is some $x:X$ such that for every $y:X$, $x=y$. Equivalently, $X$ is contractible if it is a Pointed H-Prop.