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.

翻译：我们发展了双范畴类型理论的语义与句法。双范畴类型理论包含语境、类型、项以及项之间的有向归约。该类型理论可自然地解释于一类结构化的双范畴中。我们首先以理解双范畴的形式发展其语义。理解双范畴的实例非常丰富；我们既研究具体实例，也研究由其他数据构造的实例类别。基于理解双范畴的概念，我们提取出双范畴类型理论的句法，即判断形式与结构性推理规则。通过在任何理解双范畴中给出解释，我们证明了这些规则的可靠性。我们工作的语义方面已在基于UniMath库的Coq证明助手中得到完整验证。