Library HoTT.Tests.bugs.github1791
PR 1791 reduced the number of universe variables for several definitions. These tests ensure that they remain reduced.
WildCat/Square.v:
WildCat/Yoneda.v:
Join/Core.v:
Join/JoinAssoc.v: