论文标题
通过良好基础的连贯性：同质类型理论中的驯服固定品质
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
论文作者
论文摘要
假设我们得到了一个图形，并希望显示其所有周期（封闭链）的属性。由于周期的子链不一定关闭，因此对周期的长度的诱导不起作用。本文得出了一个让人联想到循环诱导的原则，即该图作为当地汇合和（共同）有充分的关系的对称闭合的情况。我们表明，假设所涉及的属性足够好，则足以证明它在空周期和局部汇合处的周期中。 我们的动机和应用在同质类型理论的领域中，这使我们能够与出现在同质理论和高级理论中的高维结构一起工作，从而使连贯性成为中心问题。对于商品而言，这是特别的 - 一种自然操作，它为某种类型的任何二进制关系提供了一种新类型，并且为了表现良好，可以切断更高的结构（设置截断）。后者很难表征从商的地图类型到较高类型的类型，而几个开放问题源于这一困难。 我们在类型的理论环境中证明了关于循环的定理，并使用它来显示从设定的要素中消除1型的连贯条件，从而得出了近似值，以在自由组和下定位上打开问题。我们已经正式化了证明助手精益的主要结果。
Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of induction for cycles for the case that the graph is given as the symmetric closure of a locally confluent and (co-)well-founded relation. We show that, assuming the property in question is sufficiently nice, it is enough to prove it for the empty cycle and for cycles given by local confluence. Our motivation and application is in the field of homotopy type theory, which allows us to work with the higher-dimensional structures that appear in homotopy theory and in higher category theory, making coherence a central issue. This is in particular true for quotienting - a natural operation which gives a new type for any binary relation on a type and, in order to be well-behaved, cuts off higher structure (set-truncates). The latter makes it hard to characterise the type of maps from a quotient into a higher type, and several open problems stem from this difficulty. We prove our theorem on cycles in a type-theoretic setting and use it to show coherence conditions necessary to eliminate from set-quotients into 1-types, deriving approximations to open problems on free groups and pushouts. We have formalised the main result in the proof assistant Lean.
