{"id":"arxiv/2607.11329","url":"https://arxiv.org/abs/2607.11329","tags":["cs.PL","cs.LO","math.LO"],"score":0,"title":"Fuss-free cumulative universes: theory and practice","domain":"cs.PL","source":"arxiv","authors":["Raphaël Sterbac","Jonathan Sterling"],"reviews":0,"subject":"cs.PL","summary":"Universes are central to dependent type theory, and they are notoriously difficult to handle in a way that is both correct and usable. We propose a new \"fuss-free\" generalised algebraic presentation for polymorphic cumulative universes that dispenses with the intricate theory of coherent universe coercions in favour of a simpler formulation, which we prove equivalent by means of a normalisation theorem for the former. Evidence for the utility of the fuss-free formulation is provided in the form of (1) an abstract specification of its bidirectional elaboration algorithm, and (2) a concrete…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-13","reactions":{}}