The type of 2-element types

As an application of the previous post on characterizing the identity types of a type, let us show that for a type $X$ which is merely equal to the type $\mathbf{2}$ of booleans, to show that $\mathbf{2}={}X$ it is equivalent to provide a point in $X$ . Intuitively, by giving a point in $X$ , the equivalence is completely determined by mapping $1:\mathbf{2}$ to that point.

This fact about the type of 2-element types was the starting point of the definition of the real projective spaces, which I did with Ulrik Buchholtz, and we hope to publish this work soon on the arxiv. I place this post in the ‘folklore’ category, because it is basically a rephrasing of known facts, but this is joint work with Ulrik.

Recall that we have a type family $(n:\mathbb{N})\mapsto{}\mathbf{n}$ , where $\mathbf{n}$ is the canonical type with $n$ terms. The type of n-element types is then the subtype $U_n:=\Sigma_{(A:U)}~\|A=\mathbf{n}\|$ of the universe. Note that by the univalence axiom it follows immediately that the loop space $\mathbf{n}=\mathbf{n}$ of the type of n-element types is equivalent to the type $\mathbf{n}\simeq{}\mathbf{n}$ , which is a set that comes with the group structure of the symmetric group $\Sigma_n$ .

So, we already know the loop space of the type of 2-element types: it is $\Sigma_2$ (and of course it is the same as $\mathbb{Z}_2$ ). Nevertheless, by characterizing the type $\mathbf{2}=X$ for any 2-element type $X$ , we get a bit more information, and we shall see as an application at the end that we can establish the type of 2-element types as a certain classifier.

To characterize the identity type $\mathbf{2}=X$ , we have to do three things: (1) we need to give a type family $P:U_2\to{}U$ ; (2) we need to give a point $x_0:P(\mathbf{2})$ ; and (3) we need to show that the total space of $P$ is contractible. Since we have suggested already that to give an equivalence $\mathbf{2}\simeq{}X$ it is enough to tell where $1:\mathbf{2}$ is mapped to, we will take $P:U_2\to{}U$ given by $P(X):=X$ . This has the point $1:P(\mathbf{2})$ . Note that the total space $\Sigma_{(X:U_2)}~X$ of $P$ is just the type of pointed 2-element types! Its contractibility is the following theorem.

Theorem 1. The type of pointed 2-element types is contractible.

Proof. We take $(\mathbf{2},1)$ as the center of contraction. We need to define an identification of type $(\mathbf{2},1)=(X,x)$ , for any $X:U_{\mathbf{2}}$ and $x:X$ . Let $X:U_{\mathbf{2}}$ and $x:X$ . It is a standard fact that we have an equivalence of type

$\Big((\mathbf{2},1)=(X,x)\Big)\simeq{}\Big(\Sigma_{(e:\mathbf{2}\simeq{}X)}~e(1)=x\Big)$ .

Hence we can complete the proof by constructing a term of type $\Sigma_{(e:\mathbf{2}\simeq{}X)}~e(1)=x$ .

It is time for a little trick. Instead of constructing a term the type in the above type, we will show that this type is contractible. Since being contractible is a mere proposition, this allows us to eliminate the assumption $\|\mathbf{2}=X\|$ into the assumption $p:\mathbf{2}=X$ . Note that the endpoint of $p$ is free. Therefore we eliminate $p$ into $\mathsf{refl}(\mathbf{2})$ . Thus, we see that it suffices to show that the type

$\Sigma_{(e:\mathbf{2}\simeq{}\mathbf{2})}~e(1)=x$

is contractible for any $x:\mathbf{2}$ . This can be done by case analysis on $x:\mathbf{2}$ . Since we have the equivalence $\mathsf{neg}:\mathbf{2}\simeq{}\mathbf{2}$ which swaps $1$ and $0$ , it follows that $\Sigma_{(e:\mathbf{2}\simeq{}\mathbf{2})}~e(1)=1$ is contractible if and only if $\Sigma_{(e:\mathbf{2}\simeq\mathbf{2})}~e(1)=0$ is contractible. Therefore, we only need to show that the type

$\Sigma_{(e:\mathbf{2}\simeq{}\mathbf{2})}~e(1)=1$

is contractible. For the center of contraction we take $(\mathrm{id}_{\mathbf{2}},\mathsf{refl}(1))$ . It remains to construct a term of type

$\Pi_{(e:\mathbf{2}\simeq\mathbf{2}}\Pi_{(p:e(1)=1)}~(e,p)=(\mathrm{id}_{\mathbf{2}},\mathsf{refl}(1))$ .

Let $e:\mathbf{2}\simeq\mathbf{2}$ and $p:e(1)=1$ . Then we have an equivalence of type

$\Big((e,p)=(\mathrm{id}_{\mathbf{2}},\mathsf{refl}(1))\Big)\simeq{}\Big(\Sigma_{(h:e\sim{}\mathrm{id}{\mathbf{2}})}~p=h(1)\Big)$

Hence it suffices to construct a term of the type on the right hand side. We define a homotopy $h:e\sim{}\mathrm{id}_{\mathbf{2}}$ by case analysis: we take $h(1):= p$ . To define $h(0)$ , note that the type $\mathsf{fib}_{e}(0)$ is contractible. Therefore, we have a center of contraction $(x,q):\mathsf{fib}_e(0)$ . Recall that equality on $\mathbf{2}$ is decidable, so we have a term of type $(x=1)+(x=0)$ . Since $e(1)=1$ , it follows that $x=0$ . Thus, we get $e(0)=0$ , which we use to define $h(0)$ . QED

By the above theorem, we have characterized the identity type of $U_2$ . Let’s summarize the result:

Corollary 2. The canonical fiberwise map of type $\Pi_{(X:U_2)}~(\mathbf{2}=X)\to{}X$ that is determined by mapping $\mathsf{refl}_{\mathbf{2}}$ to $1:\mathbf{2}$ , is a fiberwise equivalence.