同部积在 homotopy 类型论中的研究

我们为 homotopy 类型论中的（homotopy）列积理论做出贡献。本工作的核心在于刻画类型宇宙中（图索引）列积与该宇宙切片中的列积（称为切片列积）之间的关系。为推导该刻画，我们给出一种旨在揭示这一关系的切片列积构造方法。我们利用该构造方法证明了从切片到原宇宙的忘却函子能够在树形图上创造列积。我们也利用它来研究切片列积如何与正交因子分解系统以及上同调理论相互作用。由于与正交因子分解系统的相互作用，所有指向类型（pointed type）的列积都保持 $n$-连通性，这意味着Buchholtz、van Doorn 和 Rijke 所定义的更高群在列积下封闭。我们已在Agda代码中正式化了本工作的主要内容（见 https://github.com/PHart3/colimits-agda），包括我们关于切片列积函子的主要构造。