Connected CW complexes

[aljungstrom]

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...

[Trebor-Huang]

Pasting lemmas would be really nice to have. Is this PR ready for merging?

[aljungstrom]

Pasting lemmas would be really nice to have. Is this PR ready for merging?

I agree:-) I think this one is for Anders to review but he's on parental leave.

But let's ping him just to harass him a bit ;-) @mortberg

[felixwellen]

Who else would be a candidate to review it? Maybe @ecavallo and I can do it together once we are back from vacation? Or @rwbarton ?
Or did Anders insist on reviewing it himself?

[aljungstrom]

No, anyone could do it I guess. It's a project that Anders is part of which is why I thought it'd be easier if he did it. But it doesn't matter to me.

[felixwellen]

Cool stuff!
We have only some minor requests for more comments/renamings.

[aljungstrom]

@felixwellen Thanks for reviewing! I think I've seen to all the comments now.

[felixwellen]

Yes, great!