一句话：提出一种依赖类型论，其模型恰为弱 ω-范畴，并给出粘贴方案的类型论刻画与证明系统实现。
本文研究如何用类型论刻画弱 ω-范畴。作者推广 Brunerie 关于 ω-群胚的定义，采用 Maltsiniotis（受 Grothendieck 启发）的进路，将 ω-范畴视为在所谓 coherator 范畴上保持 globular 余极限的预层；coherator 编码了粘贴方案的所有复合及其相干性。核心贡献是给出粘贴方案作为可由推理规则导出的语境（contexts）的典范类型论刻画，从而把范畴结构组织进依赖类型论。最后实现了相应的证明系统。
We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an ω-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.