一句话：为立方类型论中的若干高阶归纳类型给出构造性语义与语法扩展，并证明判断性计算规则和宇宙封闭性。
本文研究如何在立方类型论中为高阶归纳类型提供构造性基础。立方类型论已能构造性地辩护单价公理等同伦类型论原则，但球面、环面、悬挂、截断、推出等高阶归纳类型尚缺统一的语义与语法处理。作者在受立方集合启发的预层 topos 中建立构造性语义模型，并据此扩展立方类型论的语法，加入上述高阶归纳类型。该语义辩护所有这些类型构造子，且为包括高维构造子在内的全部构造子给出判断性计算规则；同时，宇宙在这些类型构造下封闭，从而在同伦类型论框架内保持计算性质。
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.