一句话：证明外延 Martin-Löf 类型论构成自由 CwF，并归约证明自由局部笛卡尔闭范畴中等式不可判定。
论文研究带外延 identity type、unit 类型 N1、Sigma 类型、Pi 类型和一个 base type 的 Martin-Löf 类型论的语义与等式判定问题。作者证明该理论在 1- 与 2-范畴意义下都是支持这些类型构造子的自由 category with families (CwF)；结合已有的 biequivalence，可推出其上下文范畴是 2-范畴意义下的自由局部笛卡尔闭范畴。随后，作者把该范畴中的等式判定归约到组合逻辑中可转换性的不可判定性，从而证明等式不可判定。基本相同的构造还给出带一个 universe 的外延 Martin-Löf 类型论中等式不可判定这一结果的略强形式。
We show that a version of Martin-L\"of type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic. Essentially the same construction also shows a slightly strengthened form of the result that equality in extensional Martin-L\"of type theory with one universe is undecidable.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CastellanCD17,
title = {Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)},
author = {Simon Castellan and Pierre Clairambault and Peter Dybjer},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:22)2017}
}