As an application of the previous post on characterizing the identity types of a type, let us show that for a type which is merely equal to the type of booleans, to show that it is equivalent to provide a point in . Intuitively, by giving a point in , the equivalence is completely determined by mapping 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 , where is the canonical type with terms. The type of n-element types is then the subtype of the universe. Note that by the univalence axiom it follows immediately that the loop space of the type of n-element types is equivalent to the type , which is a set that comes with the group structure of the symmetric group .
So, we already know the loop space of the type of 2-element types: it is (and of course it is the same as ). Nevertheless, by characterizing the type for any 2-element type , 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 , we have to do three things: (1) we need to give a type family ; (2) we need to give a point ; and (3) we need to show that the total space of is contractible. Since we have suggested already that to give an equivalence it is enough to tell where is mapped to, we will take given by . This has the point . Note that the total space of 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 as the center of contraction. We need to define an identification of type , for any and . Let and . It is a standard fact that we have an equivalence of type
Hence we can complete the proof by constructing a term of type .
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 into the assumption . Note that the endpoint of is free. Therefore we eliminate into . Thus, we see that it suffices to show that the type
is contractible for any . This can be done by case analysis on . Since we have the equivalence which swaps and , it follows that is contractible if and only if is contractible. Therefore, we only need to show that the type
is contractible. For the center of contraction we take . It remains to construct a term of type
Let and . 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 by case analysis: we take . To define , note that the type is contractible. Therefore, we have a center of contraction . Recall that equality on is decidable, so we have a term of type . Since , it follows that . Thus, we get , which we use to define . QED
By the above theorem, we have characterized the identity type of . Let’s summarize the result:
Corollary 2. The canonical fiberwise map of type that is determined by mapping to , is a fiberwise equivalence.
As an application, we show that the map pointing to classifies the double covers. By this, we mean the following:
Theorem 3. For any double cover , the square
commutes, and is a pullback.
Proof. Since for any , we have corollary 2 a fiberwise equivalence
indexed by . 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.