一句话：在 HoTT 中形式化证明序列余极限与 Σ-类型可交换，并推出若干推论。
序列余极限是同伦类型论中高阶归纳类型的重要一类。本文针对“序列余极限是否与 Σ-类型适当交换”的猜想，给出一个自包含且完全形式化的证明。基于该主定理，作者得到若干简短推论：序列余极限与恒等类型、同伦纤维、环路空间及截断交换，并在序列余极限下保持截断性与连通性，其中部分推论此前仅为猜测。整套发展还可借助 Shulman 将同伦类型论解释到 (∞,1)-拓扑斯的工作，迁移到 (∞,1)-拓扑斯中。
Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us to give short proofs of a number of useful corollaries, some of which were conjectured in other works: the commutativity of sequential colimits with identity types, with homotopy fibers, loop spaces, and truncations, and the preservation of the properties of truncatedness and connectedness under sequential colimits. Our entire development carries over to (∞, 1)-toposes using Shulman's recent interpretation of homotopy type theory into these structures.
DOI 原文 ·
@inproceedings{paperbot5538,
title = {Sequential Colimits in Homotopy Type Theory},
author = {Kristina Sojakova and Floris van Doorn and Egbert Rijke},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394801}
}