类型依赖的组合结构
Combinatorial structure of type dependency
摘要：
我们给出了一个帐户的基本组合结构的概念类型依赖。我们这样做是考虑范畴的所有依赖的代数演算，并展示它作为范畴的代数单子上的一个预层范畴。预层范畴的对象编码了一个依赖型组合演算的基本判断，而单子的作用编码了演绎规则;因此，通过给出单子的显式描述，我们得到了类型依赖的组合学的显式说明。我们发现，这种组合是由一种特殊的装饰有序树，熟悉的计算机科学和无辜的游戏语义。此外，我们发现所讨论的单子是一种特别好的单子：它是斯特里特-韦伯意义上的局部右伴随。在未来的工作中，我们将利用这一事实来描述依赖类型理论的神经，并使用二维单子理论的工具来研究依赖类型理论的一致性问题。
英文摘要：
We give an account of the basic combinatorial structure underlying the notion of type dependency. We do so by considering the category of all dependent sequent calculi, and exhibiting it as the category of algebras for a monad on a presheaf category. The objects of the presheaf category encode the basic judgements of a dependent sequent calculus, while the action of the monad encodes the deduction rules; so by giving an explicit description of the monad, we obtain an explicit account of the combinatorics of type dependency. We find that this combinatorics is controlled by a particular kind of decorated ordered tree, familiar from computer science and from innocent game semantics. Furthermore, we find that the monad at issue is of a particularly well-behaved kind: it is local right adjoint in the sense of Street--Weber. In future work, we will use this fact to describe nerves for dependent type theories, and to study the coherence problem for dependent type theory using the tools of two-dimensional monad theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
