Explicitly enable universe checking #17
Description
If UniMath/UniMath#1697 or something similar is merged, then importing UniMath here will disable universe checking (i.e. effectively enable -type-in-type) in this development as well. So it should be (re-)enabled here, probably by adding Export Set Universe Checking in prelude.imports or prelude.prelude.
See also more discussion in UniMath/UniMath#1696.