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.