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.
Merge pull request #401 from JasonGross/less-pointwise-paths-universes

Don't have an extra universe in [pointwise_paths]