Search papers, labs, and topics across Lattice.
This paper introduces a novel proof technique rooted in domain theory to establish definitional inversion properties鈥攕pecifically injectivity and no-confusion of type constructors鈥攊n 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 in the presence of $\eta$ laws. By addressing the complexities of non-normalizing systems like Idris and Lean, this work lays the groundwork for advancing the metatheory of various dependent type systems and their extensions.
Injectivity of type constructors can be proven in non-normalizing dependent type systems, a breakthrough for the metatheory of languages like Idris and Lean.
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.
