TY - RPRT TI - Bounded First-Class Universe Levels in Dependent Type Theory AU - Jonathan Chan AU - Stephanie Weirich PY - 2025 UR - https://arxiv.org/abs/2502.20485 ID - 2502.20485 ER -