{"ID":6537606,"CreatedAt":"2026-07-14T02:54:43.516908796Z","UpdatedAt":"2026-07-15T03:28:55.185153975Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.11329","arxiv_id":"2607.11329","title":"Fuss-free cumulative universes: theory and practice","abstract":"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 implementation in Haskell. We also describe and implement an extension of the fuss-free universe hierarchy with a judgemental notion of datatype description from which prior notions of cumulative inductive type may be derived.","short_abstract":"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...","url_abs":"https://arxiv.org/abs/2607.11329","url_pdf":"https://arxiv.org/pdf/2607.11329v1","authors":"[\"Raphaël Sterbac\",\"Jonathan Sterling\"]","published":"2026-07-13T09:48:19Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.LO\",\"math.LO\"]","methods":"[]","has_code":false}