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.
Theorem 8.2.1.
If is -connected then the suspension of is -connected.
Proof.
We remarked in \\autorefsec:colimits that the suspension of is the pushout , so we need toprove that the following type is contractible:
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 mapis an equivalence
where we recall that is the type
The map is an equivalence, hencewe also have
Now is -connected hence so is because, and is -truncated because is -connected. Hence by \\autorefconnectedtotruncated thefollowing map is an equivalence
Hence we have
But the following map is an equivalence
Hence
Finally we get an equivalence
We can now unfold the definitions in order to get the explicit expression ofthis map, and we see easily that this is exactly the map we had at thebeginning.
Hence we proved that is a pushout of in . Usinguniqueness of pushouts we get that which proves that the suspension of is -connected.∎
Corollary 8.2.2.
For all , the sphere is -connected.
Proof.
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.∎