2.8 The unit type

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

Theorem 2.8.1.

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

Proof.

A function $(x=y)\to \mathrm{𝟏}$ is easy to define by sending everything to $\star$.Conversely, for any $x,y:\mathrm{𝟏}$ we may assume by induction that $x\equiv \star \equiv y$.In this case we have ${\mathrm{𝗋𝖾𝖿𝗅}}_{\star }:x=y$, yielding a constant function $\mathrm{𝟏}\to (x=y)$.

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

On the other hand, suppose given $p:x=y$.By path induction, we may assume $x\equiv y$ and $p$ is ${\mathrm{𝗋𝖾𝖿𝗅}}_x$.We may then assume that $x$ is $\star$, in which case the composite $(x=y)\to \mathrm{𝟏}\to (x=y)$ takes $p$ to ${\mathrm{𝗋𝖾𝖿𝗅}}_x$, i.e. to $p$.∎

In particular, any two elements of $\mathrm{𝟏}$ 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 $\mathrm{𝟏}$ is simply the transport lemma for constant type families (Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrations#Thmlem4)).