Connectedness, TruncType

Various additions:

- completed proof of connectedness of wedge-into-product, modulo lemma on connectedness of the basepoint inclusion;
- added `TruncType.v`, defining the universe of n-truncated types and showing that it is (n+1)-truncated;
- various other lemmas, tactics, etc.

There are a few things I’m slightly unhappy about in this code — naming, placement of auxiliary lemmas, etc — mostly in `TruncType`, and flagged/described in comments with `TODO`.  Issuing pull request nonetheless in hopes that other pairs of eyes may see solutions that are eluding me!