空间值图，类型理论（扩展抽象）
Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
摘要：
拓扑学家有时对给定索引范畴上的空值图感兴趣，但如果我们寻找一个在等价下稳定的概念，那么要说这样的图是什么是很棘手的。在（同伦）类型论中也是如此，只有在特殊情况下，人们才知道如何在给定的索引范畴上定义一种类型值图。我们提供几种结构。我们首先展示了如何定义同伦相干图来与所有更高的一致性法律明确，有两个变种，来与假设的指数范畴或类型理论。此外，我们提出了一个建设的图表在某些里德类别。作为一个应用程序，我们添加的退化到著名的建设半单纯型，产生一个建设单纯型到任何给定的有限水平。目前的论文只是一个扩展的摘要，完整的版本将遵循。在全文中，我们将表明，不同的概念的图是等价的，彼此和已知的概念Reedy conjugant图时，声明是有意义的。在本文中，我们只勾画了一些证明的核心思想。
英文摘要：
Topologists are sometimes interested in space-valued diagrams over a given index category, but it is tricky to say what such a diagram even is if we look for a notion that is stable under equivalence. The same happens in (homotopy) type theory, where it is known only for special cases how one can define a type of type-valued diagrams over a given index category. We offer several constructions. We first show how to define homotopy coherent diagrams which come with all higher coherence laws explicitly, with two variants that come with assumption on the index category or on the type theory. Further, we present a construction of diagrams over certain Reedy categories. As an application, we add the degeneracies to the well-known construction of semisimplicial types, yielding a construction of simplicial types up to any given finite level. The current paper is only an extended abstract, and a full version is to follow. In the full paper, we will show that the different notions of diagrams are equivalent to each other and to the known notion of Reedy fibrant diagrams whenever the statement makes sense. In the current paper, we only sketch some core ideas of the proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
