论文标题
依赖类型理论的句法类别：素描和充分性
Syntactic categories for dependent type theory: sketching and adequacy
论文作者
论文摘要
我们认为，本地笛卡尔封闭类别构成了用于定义依赖类型理论（包括非扩展理论）的合适学说。使用草图理论，可以按照“判断为类型”的原理来定义类型的类型理论的句法类别。类型理论集中在其本地笛卡尔封闭类别的判断类别中，对于通过语义手段（规范性，归一化等）证明句法元看序列特别方便。也许令人惊讶的是，从这种意义上讲，上下文的概念在类型理论的定义中没有任何作用，但是在需要的任何地方，都可以将一类显示图的结构强加于事实上的理论，并由爱丁堡学校所提倡，并由百分比的Twelf Pircept Assister的宣言实现。 Uemura提出了可代表的地图类别以及用于类似目的的分层逻辑框架。 Uemura框架中的分层限制了使用依赖产品的使用是严格的积极的，与Martin-Löf的逻辑框架和Schroeder-Heister对高层推论的分析相比。我们证明了相对于Uemura代表地图类别的本地笛卡尔封闭类别的语义足够结果：如果在Uemura的框架中可以定义理论，则它生成的本地笛卡尔封闭类别是保守的（完全忠实的）其stancactic Abledable Map类别。在此基础上，我们主张将本地笛卡尔封闭类别用作Uemura代表地图类别的更简单替代品。
We argue that locally Cartesian closed categories form a suitable doctrine for defining dependent type theories, including non-extensional ones. Using the theory of sketches, one may define syntactic categories for type theories in a style that resembles the use of Martin-Löf's Logical Framework, following the "judgments as types" principle. The concentration of type theories into their locally Cartesian closed categories of judgments is particularly convenient for proving syntactic metatheorems by semantic means (canonicity, normalization, etc.). Perhaps surprisingly, the notion of a context plays no role in the definitions of type theories in this sense, but the structure of a class of display maps can be imposed on a theory post facto wherever needed, as advocated by the Edinburgh school and realized by the %worlds declarations of the Twelf proof assistant. Uemura has proposed representable map categories together with a stratified logical framework for similar purposes. The stratification in Uemura's framework restricts the use of dependent products to be strictly positive, in contrast to the tradition of Martin-Löf's logical framework and Schroeder-Heister's analysis of higher-level deductions. We prove a semantic adequacy result for locally Cartesian closed categories relative to Uemura's representable map categories: if a theory is definable in the framework of Uemura, the locally Cartesian closed category that it generates is a conservative (fully faithful) extension of its syntactic representable map category. On this basis, we argue for the use of locally Cartesian closed categories as a simpler alternative to Uemura's representable map categories.
