feat(hott/init): make sure eq is universe polymorphic

Jakob and Floris needed path equality to be universe polymorphic when
proving univalence.
feat(hott/init): make sure eq is universe polymorphic