Typed two dimensional lambda calculus clarifies equality evidence
A Theory of a Two-Dimensional Typed Lambda Calculus
Logic in Computer Science
Summary
This paper introduces a new way to track how computer programs written in a typed lambda calculus are considered equal. Instead of saying two programs are equal by default, the authors show equality as a clear step-by-step transformation between them. They build a two-dimensional system that can manage these transformations explicitly, improving on traditional theories that rely on less constructive methods. Their system is carefully tested in a programming language called Idris 2 and offers new insights about how syntax (the form of code) relates to semantics (its meaning).
What this means in practice
- •For programming language designers: Incorporate computationally explicit equality evidence into type systems to improve program verification and proof management.
- •For proof assistant developers: Develop tools that use explicit step sequences for equality, enabling more fine-grained and intensional reasoning about programs and proofs.
A theory result. No direct application yet.
Authors
Daniel O. Martínez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Abstract
We present a typed two-dimensional $λ$-calculus whose equality evidence is \emph{computational}: a path between two terms is an explicit finite sequence of one-step conversions (the $β$- and $η$-contractions, the congruences, and the structural rules), and every property of paths is proved \emph{by recursion over that sequence}, with any step as a base case --- in deliberate contrast with Martin-Löf type theory, where identity is generated by reflexivity alone and all properties go through the non-computational $J$-eliminator. The higher structure is imported from the $2β$- and $2η$-conversions of the theory of an arbitrary higher $λ$-model: we obtain 2-dimensional coherence laws, computable naturality of homotopies (via inductive homotopies and their explicit evaluations), a 2-dimensional path type with transport, and a parity invariant that proves the system consistent and \emph{really intensional}: the $β$- and $η$-contractions are provably distinct evidence, while in the native syntax of Idris (core MLTT) they are identified by definitional equality. Commutative diagrams accompany the main constructions, and the theory is fully formalized in Idris 2. A parallel Lean formalization is published in the Palomar registry \cite{palomar2026lean}. A philosophical reading closes the paper: constructivism in the BHK sense, proof-relevant intensionality, and the boundary between syntax and semantics, drawn relative to MLTT and HoTT.}