Generalize Lemma 2.4.2 to dependent functions, close #486
Merge pull request #734 from mikeshulman/homotopies

Generalize Lemma 2.4.2 to dependent functions, close #486