Fuss-free cumulative universes: theory and practice

Raphaël Sterbac; Jonathan Sterling

Fuss-free cumulative universes: theory and practice

Programming Languages 2026-07-13 v1 Logic in Computer Science Logic

Authors: Raphaël Sterbac , Jonathan Sterling

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.

Keywords

dependent type theory cumulative universes generalized algebraic presentation normalization theorem bidirectional elaboration Haskell implementation

Cite

@article{arxiv.2607.11329,
  title  = {Fuss-free cumulative universes: theory and practice},
  author = {Raphaël Sterbac and Jonathan Sterling},
  journal= {arXiv preprint arXiv:2607.11329},
  year   = {2026}
}