Paper: Definitional Proof Irrelevance Made Accessible (at LICS 2026)

Authors: Thiago Felicissimo Yann Leray Loïc Pujet Nicolas Tabareau Éric Tanter Théo Winterhalter

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.41

Abstract

A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates - used to establish semantic termination arguments - to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, with two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof made in the definitional variant of the theory can be translated into a proof of the same statement in the propositional variant, all while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.

BibTeX

  @InProceedings{FelicissimoLerayPuj-DefinitionalProofIr,
    author = 	 {Thiago Felicissimo and Yann Leray and Loïc Pujet and Nicolas Tabareau and Éric Tanter and Théo Winterhalter},
    title = 	 {Definitional Proof Irrelevance Made Accessible},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {41:1--41:26},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.41}
  }