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.