一句话：在函数外延性与参数性假设下，证明 Leibniz 相等与 Martin-Löf 同一性之间的互转构成同构。
本文比较 Leibniz 相等与 Martin-Löf 同一性这两种等义定义：前者用谓词保持刻画相等，后者用同一类型是否有居留刻画。已有工作知道二者可互相证明，但本文在类型论内部证明两个方向的转换互为逆，从而构成同构。其中一个方向的关键依赖是相应 Leibniz 相等类型满足函数外延性和 Reynolds 参数性。该结论是一般性的归纳族与其 Church 编码之间关系的一个特例。全部证明以 literate Agda 脚本机器化完成，而非元理论论证。
Abstract Consider two widely used definitions of equality. That of Leibniz: one value equals another if any predicate that holds of the first holds of the second. And that of Martin-Löf: the type identifying one value with another is occupied if the two values are identical. The former dates back several centuries, while the latter is widely used in proof systems such as Agda and Coq. Here we show that the two definitions are isomorphic: we can convert any proof of Leibniz equality to one of Martin-Löf identity and vice versa , and each conversion followed by the other is the identity. One direction of the isomorphism depends crucially on values of the type corresponding to Leibniz equality satisfying functional extensionality and Reynolds’ notion of parametricity. The existence of the conversions is widely known (meaning that if one can prove one equality then one can prove the other), but that the two conversions form an isomorphism (internally) in the presence of parametricity and functional extensionality is, we believe, new. Our result is a special case of a more general relation that holds between inductive families and their Church encodings. Our proofs are given inside type theory, rather than meta-theoretically. Our paper is a literate Agda script.
@article{AbelCDTW20,
title = {Leibniz equality is isomorphic to Martin-Löf identity, parametrically},
author = {ANDREAS ABEL and JESPER COCKX and DOMINIQUE DEVRIESE and AMIN TIMANY and PHILIP WADLER},
journal = {Journal of Functional Programming},
volume = {30},
year = {2020},
doi = {10.1017/s0956796820000155}
}