论文标题
主教型理论：语义和语法
Bicategorical type theory: semantics and syntax
论文作者
论文摘要
我们开发了用于生物构想理论的语义和语法。主教型理论具有上下文，类型，术语和术语之间的定向减少。这种类型的理论自然在一类结构化的生物学中解释。我们首先以理解生物学的形式开发语义。理解生物学的例子很多；我们研究了从其他数据构建的特定示例以及示例类别。从理解生物学的概念中，我们提取了生物类型理论的语法，即判断形式和结构推理规则。我们通过在任何理解的生物学中给出解释来证明规则的健全性。根据Unimath库，在COQ证明助手中完全检查了我们作品的语义方面。
We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.
