More equivalences.

We introduce some alternative models for equivalences, some of which
are easier to prove, as discussed in the Homotopy Type Theory book.

As an application, we prove that composites of n-truncated maps are
n-truncated.