HoTT/HoTT — pull request #116 by peterlefanulumsdaine (2013-04-10 16:19:39+00:00)
Title: Suspensions, spheres, connectedness, and a start on Freudenthal

Various work on HIT’s, towards the goal of Freudenthal. Issuing pull request even though that goal isn’t reached yet, so that the auxiliary work done (spheres etc.) doesn’t get duplicated in master.

I’m keeping `Freudenthal.v` itself in `/contrib/` for now, since it’s still full of loose ends and very liable to change.

There are several miscellaneous definitions/lemmas whose placement I’m not happy with, e.g. NullHomotopy (currently in `Spheres.v`), and the auxiliary lemmas in `TruncTypes.v`. If anyone can find better homes for these, I’d be happy!

In general, I’ve been increasingly feeling that we’ve outgrown the current library organisation. (Specifically: I keep on having trouble working out the right homes for things, either because they don’t naturally fit in any major thematic threads but aren’t so basic they belong in Overture, or because they have dependencies that prevent them from going where they thematically fit.) Have others been getting the same feeling? If so, it might be helpful to have some more discussion about the library organisation, once the current urgency on the book is past.