HoTT/HoTT — pull request #659 by mikeshulman (2014-12-29 22:48:10+00:00)
Title: path-spaces of truncations (Theorem 7.3.12)

I was surprised that we didn't have this yet. (Unless I missed it?)