8.2 Connectedness of suspensions
Recall from \autorefsec:connectivity that a type is called -connected if is contractible. The aim of this section is to prove that the operation of suspension from \autorefsec:suspension increases connectedness.
If is -connected then the suspension of is -connected.
By \autorefreflectcommutespushout we know that is a pushout in of the diagram
Given that , the type is also a pushout of the following diagram in (because both diagrams are equal)
We will now prove that is also a pushout of in . Let be an -truncated type; we need to prove that the following map is an equivalence
where we recall that is the type
The map is an equivalence, hence we also have
Now is -connected hence so is because , and is -truncated because is -connected. Hence by \autorefconnectedtotruncated the following map is an equivalence
Hence we have
But the following map is an equivalence
Finally we get an equivalence
We can now unfold the definitions in order to get the explicit expression of this map, and we see easily that this is exactly the map we had at the beginning.
Hence we proved that is a pushout of in . Using uniqueness of pushouts we get that which proves that the suspension of is -connected. ∎
For all , the sphere is -connected.
We prove this by induction on . For we have to prove that is merely inhabited, which is clear. Let be such that is -connected. By definition is the suspension of , hence by the previous lemma is -connected. ∎
|Title||8.2 Connectedness of suspensions|