自由局部笛卡尔闭范畴中等式的不可判定性（扩展版）
计算机科学中的逻辑
2019-03-14 v3
摘要
我们证明了带有外延同一类型构造子I、单位类型N1、Sigma类型、Pi类型和一个基类型的Martin-Löf类型理论的一个版本，在1-和2-范畴意义上都是一个自由带族范畴（支持这些类型构造子）。由此，由于先前证明的双向等价，上下文的底范畴在2-范畴意义下是一个自由局部笛卡尔闭范畴。我们通过将其归约到组合子逻辑中可转换性的不可判定性，证明了该范畴中的等式是不可判定的。本质上相同的构造也展示了一个稍强化的结果：带有一个全集的外延Martin-Löf类型理论中的等式是不可判定的。
引用
@article{arxiv.1504.03995,
title = {Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)},
author = {Simon Castellan and Pierre Clairambault and Peter Dybjer},
journal= {arXiv preprint arXiv:1504.03995},
year = {2019}
}