# 2.8 The unit type

Trivial cases are sometimes important, so we mention briefly the case of the unit type $\mathbf{1}$.

###### Theorem 2.8.1.

For any $x,y:\mathbf{1}$, we have $(x=y)\simeq\mathbf{1}$.

###### Proof.

A function $(x=y)\to\mathbf{1}$ is easy to define by sending everything to $\star$. Conversely, for any $x,y:\mathbf{1}$ we may assume by induction that $x\equiv\star\equiv y$. In this case we have $\mathsf{refl}_{\star}:x=y$, yielding a constant function $\mathbf{1}\to(x=y)$.

To show that these are inverses, consider first an element $u:\mathbf{1}$. We may assume that $u\equiv\star$, but this is also the result of the composite $\mathbf{1}\to(x=y)\to\mathbf{1}$.

On the other hand, suppose given $p:x=y$. By path induction, we may assume $x\equiv y$ and $p$ is $\mathsf{refl}_{x}$. We may then assume that $x$ is $\star$, in which case the composite $(x=y)\to\mathbf{1}\to(x=y)$ takes $p$ to $\mathsf{refl}_{x}$, i.e. to $p$. ∎

In particular, any two elements of $\mathbf{1}$ are equal. We leave it to the reader to formulate this equivalence in terms of introduction, elimination, computation, and uniqueness rules. The transport lemma for $\mathbf{1}$ is simply the transport lemma for constant type families (Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrations#Thmlem4)).

Title 2.8 The unit type
\metatable