Singleton Type

The type of singletons of a type $A:\mathsf{U}{}$ is the Type Family

• $\mathsf{Sing}(x)=\Sigma(y:A).\;x=y$

Properties

• The type of singletons $\mathsf{Sing}(x)$ is Contractible, where the centre of contraction is $(x,\mathsf{refl})$. This is an alternative way of stating the J Rule.