AI 中文总结
提出一个二维类型化λ演算，以计算性路径作为相等性证据，通过递归证明性质，引入高阶相干律和路径类型，并用奇偶不变量证明系统一致且真正内涵，在Idris 2中完全形式化。
AI 中文摘要
我们提出一个类型化的二维λ演算，其相等性证据是计算性的：两个项之间的路径是一个显式的有限序列，由一步转换（β-和η-收缩、同余规则以及结构规则）组成，并且路径的每个性质都通过在该序列上进行递归来证明，任何一步都可作为基础情形——这与Martin-Löf类型理论形成刻意对比，后者中同一性仅由自反性生成，所有性质都通过非计算性的J-消去器处理。更高阶结构从任意高阶λ模型理论中的2β-和2η-转换引入：我们获得二维相干律、同伦的可计算自然性（通过归纳同伦及其显式求值）、带有传输的二维路径类型，以及一个奇偶不变量，该不变量证明系统是一致的且真正内涵的：β-和η-收缩是可证明地不同的证据，而在Idris（核心MLTT）的原生语法中，它们通过定义性相等被识别。交换图伴随主要构造，并且该理论在Idris 2中完全形式化。一个并行的Lean形式化已在Palomar注册表中发布。论文以哲学解读收尾：BHK意义上的构造主义、证明相关的内涵性，以及语法与语义之间的边界，相对于MLTT和HoTT进行划定。
英文摘要
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.}
