我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：提出 comprehension bicategories 作为二维类型理论的一般模型，统一并涵盖已有的 directed type theory 解释。

论文研究二维类型理论的语义模型问题。二维类型理论（如有向类型理论）需要比一维范畴语义更丰富的结构。作者提出“理解双范畴”（comprehension bicategories）作为一般模型，给出其定义并说明其如何解释二维类型理论中的类型与项结构。文中指出这类模型实例丰富，可将文献中已有的有向类型理论解释纳入该框架，从而为二维类型理论提供统一的范畴语义基础。

问题

如何为二维类型理论及有向类型理论给出统一、一般的语义模型？

方法

提出 comprehension bicategory 作为二维类型理论的一般模型，用双范畴结构刻画类型构造与其语义解释。

评估

通过展示大量 comprehension bicategory 实例，并说明已有有向类型理论解释均可纳入该框架，论证其一般性与适用性。

链接与引用

DOI 原文 · PDF（开放获取） ·

@inproceedings{paperbot6707,
  title = {Semantics for two-dimensional type theory},
  author = {Benedikt Ahrens and Paige Randall North and Niels van der Weide},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533334}
}