经由良基性的 coherence：驯服同伦类型论中的集合商
逻辑
2020-07-01 v2 计算机科学中的逻辑
组合数学
摘要
假设给定一个图并希望证明其所有环（闭链）的一个性质。对环长度进行归纳无法奏效，因为环的子链未必是闭的。本文针对图由局部合流且（共）良基关系的对称闭包给出的情况，推导出一个类似于环归纳的原理。我们证明，若所讨论的性质足够良好，则只需对空环与由局部合流给出的环证明该性质即可。我们的动机与应用在于同伦类型论领域，该理论使我们能处理同伦论与高阶范畴论中出现的高维结构，使coherence成为核心问题。这对取商尤为如此——取商是一种自然操作，对类型上的任意二元关系给出一个新类型，且为了行为良好会截断高维结构（集合截断）。后者使得刻画从商到高阶类型的映射类型变得困难，若干开放问题源于此困难。我们在类型论设定中证明关于环的定理，并用它展示从集合商消去到1-型所必需的coherence条件，推导出关于自由群与推出型的开放问题的近似解。我们已在证明助手Lean中形式化了主要结果。
引用
@article{arxiv.2001.07655,
title = {Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory},
author = {Nicolai Kraus and Jakob von Raumer},
journal= {arXiv preprint arXiv:2001.07655},
year = {2020}
}
备注
v2: essentially the version published in the proceedings of Logic in Computer Science, numbering identical