In this work, we propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. 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. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.

翻译：在这项工作中,我们提出了二维理论模式的一般概念,其形式为理解两类。理解两类的例子非常丰富;其中包括对文献中以前研究过的直接类型理论的解释。我们从理解二类中为二维理论提取核心语法,即判断形式和结构推论规则。我们通过在任何可理解双类中提供解释来证明规则的正确性。我们工作的语义方面由Coq验证助理根据UnityMath图书馆进行充分检查。这是向更高维的定向类型理论提供词义学和语义学理论的第一步。