Initiated Suspension.v
Gave non-dep elim for suspension.
Suspension: basic lemmas, and a somewhat experimental start on Freudenthal.
Further progress on Suspension (except that perhaps this truncation-free approach isn’t working.
Fixed problem in prev commit.
Splitting off Freudenthal from Suspension (so that connectedness can be redefined using truncations, creating dependencies Freudenthal <- Connectedness <- Truncation <- Spheres <- Suspension).
Initiated Spheres.v, defining spheres by iterated suspension, and showing these are correct in low dimensions.
Moved NullHomotopy from Freudenthal to Spheres.
Added dependent analogue of [transport_paths_FlFr].
Added eta-rule for Suspension.
Showed that truncatedness is equivalent to maps from spheres being null-homotopic.
Initiated Truncations.v
Gave characterisation of connectedness as contractibility of truncation.
Gave equivalence of the characterisations of connected maps via elim principle and via fibers.
Added lemmas on connectedness of a pointed type.
Much progress on Freudenthal (but universe inconsistency).
Resolved universe inconsistency in Freudenthal.
Added [isequiv_cancelL], and various related changes.
Added [trunc_leq].
Further (halting) progress on Freudenthal.