This PR introduces the notion of an n-connected CW complex (in terms of trivial lower skeleta).
The main result is makeConnectedCW in CW.Connected which says that this is (merely) implied by the usual definition of connectedness. This is the main component of the proof of the Hurewicz theorem that I have in mind -- ping @rwbarton @owen-fool (we still need some other stuff first though).
Pushout squares and pasting lemmas are added to HITS.Pushout.
A bunch of minor lemmas about manipulating pushouts, cofibres, wedge sums, etc.
Many results concerning pushouts have been reparametrised with general universe levels. This makes this PR look a bit larger than it actually is...
This PR introduces the notion of an n-connected CW complex (in terms of trivial lower skeleta).
makeConnectedCWinCW.Connectedwhich says that this is (merely) implied by the usual definition of connectedness. This is the main component of the proof of the Hurewicz theorem that I have in mind -- ping @rwbarton @owen-fool (we still need some other stuff first though).HITS.Pushout.