一句话：为笛卡尔闭双范畴构造内部类型理论，将 Curry-Howard-Lambek 对应提升到双范畴情形。
论文为笛卡尔闭双范畴建立内部语言。作者引入一种类型理论来刻画笛卡尔闭双范畴的结构，并证明其语法模型满足适当的泛性质，从而把 Curry-Howard-Lambek 对应提升到双范畴情形。方法上，他们借助普适代数中 abstract clone 概念的双范畴化来构造弱代换结构，并从语义考量合成乘积与指数类型的规则。所得类型理论新颖地结合了二维类型论与显式代换，并直接推广简单类型 λ 演算。该工作是证明笛卡尔闭双范畴 coherence 这一研究计划的第一步。
We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical. Weak substitution structure is constructed using a bicategori-fication of the notion of abstract clone from universal algebra, and the rules for products and exponentials are synthesised from semantic considerations. The result is a type theory that employs a novel combination of 2-dimensional type theory and explicit substitution, and directly generalises the Simply-Typed Lambda Calculus. This work is the first step in a programme aimed at proving coherence for cartesian closed bicategories.