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


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


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


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


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


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


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.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s