Homotopies, equivalences, sets, and propositions

[Anatolay]

This PR contains the following:

• Most of Section 2.4 Homotopies and equivalences
• Most of Section 2.6 Cartesian product types
• Section 2.8 The unit type
• Definition of functional extensionality in Section 2.9 $\prod$-types and the function extensionality axiom
• Some of Section 3.1 Sets and $n$-types
  • Definition of isSet
  • Proofs that Unit, products of sets, and functions into sets are sets
  • Simplification of proofs by factoring out injective-equivalence lemma
• Some of Section 3.3 Mere propositions
  • Proofs that Unit and functions into mere propositions are mere propositions
• Definition of contractibility in Section 3.11 Contractibility

Original description:

Definitions and proofs for Section 2.4.

Depends on #11