HoTT/HoTT — pull request #401 by JasonGross (2014-05-29 19:12:36+00:00)
Title: Don't have an extra universe in [pointwise_paths]

It's not necessary. Removing it makes figuring out where universes in
Funext come from a bit easier.