Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich
cs.LO
Jul 15, 2026 · v1
cs.PL
TL;DR
Meta-theoretic proof of definitional inversion for dependent type theory is mechanised in Lean (alongside Agda and Rocq), targeting the Lean4Lean project.
Abstract
We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity and no-confusion of type constructors. This proof technique is independent of normalisation, and indeed applies even for the "type-in-type" rule of Martin-Löf's original type theory. Our proof is the first to establish injectivity of type constructors for such a system in the presence of $η$ laws. More generally, the technique is motivated by, and intended for, the metatheory of systems such as Idris, Lean, or dependent Haskell, whose underlying type theory is known to be non-normalising, as well as projects such as MetaRocq or Lean4Lean, where Gödel's second incompleteness theorem means we cannot show normalisation of the object logic in itself. We showcase the method on a small type theory, then explain how it extends to more ambitious extensions.
Problem
Standard meta-theory tools (confluence, logical relations) cannot establish definitional inversion properties (injectivity, no-confusion of type constructors) for non-normalising dependent type theories used in systems like Lean, Idris, and dependent Haskell, especially in the presence of eta laws.
Approach
A new proof technique based on domain theory constructs a domain model of type theory as a solution to a domain equation, interpreting types as finitary projectors. A logical relation between syntactic terms and semantic witnesses is used to establish model adequacy without requiring normalisation. From adequacy, injectivity of type constructors is derived, and the model deliberately collapses structure (e.g. universe levels) to scale to extensions.
Results
The technique proves injectivity of type constructors, including for type-in-type systems with eta laws, the first such result. The results were mechanised in Agda, Lean, and Rocq, with the Lean and Rocq versions intended as candidates for the Lean4Lean and MetaRocq projects.
| System | U:U | Pi | Sigma,1 | Y | N | Id |
|---|
| Agda | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ |
| Lean | ✓ | ✓ | ✓ | ✓ | ✓ | transport only |
| Rocq | ✓ | ✓ | | | 0 and S only | |
Features covered by each mechanisation
