弱$ω$-范畴的计算机化作为归纳类型
摘要：用显式的归纳定义给出了计算结构的新描述，从而对计算结构有了新的理解，并且可以避免球形操作的技术，提供了一个避免球形操作的定义。我们的框架允许通过结构归纳直接证明重要结果，我们利用这一点给出了每个$omega$-范畴都等价于一个自由范畴的新证明，并且计算结构范畴与变量到变量映射是一个预设拓扑，给出了索引范畴的直接描述。我们证明了我们得到的$omega$-范畴的定义与Batanin和Leinster的定义一致，并且所引导出的$omega$-范畴的同胚替代概念与Garner的概念一致。
作者：Christopher J. Dean, Eric Finster, Ioannis Markakis, David Reutter, Jamie Vicary
论文ID：2208.08719
分类：Category Theory
分类简称：math.CT
提交时间：2022-12-15