Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces a novel proof technique rooted in domain theory to establish definitional inversion properties—specifically injectivity and no-confusion of type constructors—in dependent type systems without relying on normalization. The technique is particularly significant as it applies to Martin-Löf's original type theory, even under the "type-in-type" rule, and is the first to demonstrate injectivity of type constructors in the presence of $\eta$ laws. By showcasing its application to a small type theory and discussing its extension to more complex systems like Idris and Lean, the authors provide a crucial advancement in the metatheory of non-normalizing type systems.
Establishing injectivity of type constructors in non-normalizing dependent type systems could revolutionize our understanding of type theory's foundational properties.
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\"of's original type theory. Our proof is the first to establish injectivity of type constructors for such a system in the presence of $\eta$ 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\"odel'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.