# 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.

As an application, we show that the map $\mathbf{1}\to U_2$ pointing to $\mathbf{2}$ classifies the double covers. By this, we mean the following:

Theorem 3. For any double cover $B:A\to{}U_2$, the square

commutes, and is a pullback.

Proof. Since $\mathsf{fib}_f(x):U_{\mathbf{2}}$ for any $x:A$, we have corollary 2 a fiberwise equivalence

$(\mathsf{2}=\mathsf{fib}_f(x))\simeq{}\mathsf{fib}_f(x)$.

indexed by $x:A$. Hence it follows that the induced map of total spaces is an equivalence. Then, it also follows that the diagram

commutes. Since the inner square is a pullback square, it follows that the outer square is a pullback square.

Advertisements