TY - RPRT TI - A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism AU - Marc Bezem AU - Thierry Coquand AU - Peter Dybjer AU - Martín Escardó PY - 2026 DO - 10.4204/eptcs.441.4 UR - https://arxiv.org/abs/2603.04010 ID - 2603.04010 ER -