A type theory for synthetic ∞-categories
A type theory for synthetic ∞-categories
复制标题
综合 ∞ 范畴的类型理论
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Michael Shulman
中科院分区：
文献类型：
--
作者：
E. Riehl;Michael Shulman
我们提出了同伦类型论中$(inty,1)$-范畴的一个综合理论的基础。我们公理化了一个有向区间类型，然后由此定义了高简式，并用它们来探测任意类型的内部范畴结构。我们定义了emph{Segal类型}，其中二元复合在同伦之前唯一存在；这自动确保了组合在所有维度上都是连贯的、统一的。我们定义了emph{Rezk类型}，其中范畴同构额外等价于类型论恒等式——一个“局部一元”条件。我们定义了在Segal类型上功能变化的类型族emph{协变纤维}，并证明了一个“依赖Yoneda引理”，它可以看作是单位类型通常消去规则的一种有向形式。通过研究Segal类型之间的同伦正确的伴随，我们得出结论，并证明Rezk类型之间的函子有伴随是一个单纯的命题。为了使这种证明中的记录易于管理，我们使用具有形状的三层类型理论，其上下文由有向立方体内的多面体扩展，可以使用“扩展类型”来抽象，该扩展类型概括了立方体类型理论的路径类型。在附录中，我们描述了二项式集上Reedy模型结构中的激励语义，其中我们的Segal和Rezk类型对应于Segal空间和完全Segal空间。
We propose foundations for a synthetic theory of $(infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define emph{Segal types}, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define emph{Rezk types}, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities --- a ``local univalence' condition. And we define emph{covariant fibrations}, which are type families varying functorially over a Segal type, and prove a ``dependent Yoneda lemma' that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using ``extension types' that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.