A basic fact in homotopy type theory is that homotopy equivalences are (coherent) equivalences. This is important because on the one hand, homotopy equivalences are the “correct” sort of equivalence, but on the other hand, for a function f the type of “homotopy equivalence data for f” is not an h-proposition. There are at least three definitions of “equivalence” which do give an h-proposition (assuming function extensionality) and are all equivalent:
- Voevodsky’s definition: all homotopy fibers are contractible.
- Adjoint equivalences: the two homotopies in a homotopy equivalence are compatible with one higher homotopy.
- h-isomorphisms: a homotopy section and a homotopy retraction.
Of these, the first two require more data than a homotopy equivalence. So in practice, when proving some map to be an equivalence, we want to be able to just show that it is a homotopy equivalence. Thus we need some way to recover that extra data if…
View original post 589 more words