一句话：从任意类型论模型构造出满足参数性的模型，并揭示参数性与半立方类型的对应。
本文研究如何从任意类型论模型出发构造满足参数性（parametricity）的模型，并建立参数性与立方结构之间的对应。核心思想是把新模型中的类型解释为旧模型中的半立方类型（semi-cubical type）。该构造不仅适用于参数性，也适用于类型论的类似解释，甚至任意广义代数理论的类似解释。更精确地，作者考虑一个遗忘函子，它忘记广义代数理论中的一元操作以及递归定义这些操作的等式，并证明该函子具有右伴随。技术工具包括局部可表现范畴论以及商归纳-归纳类型（quotient inductive-inductive types）。关键结果是得到一种统一的范畴论构造，使参数性与半立方类型之间的对应成为一般现象。
We construct a model of type theory enjoying parametricity from an arbitrary one. A type in the new model is a semi-cubical type in the old one, illustrating the correspondence between parametricity and cubes.Our construction works not only for parametricity, but also for similar interpretations of type theory and in fact similar interpretations of any generalized algebraic theory. To be precise we consider a functor forgetting unary operations and equations defining them recursively in a generalized algebraic theory. We show that it has a right adjoint.We use techniques from locally presentable category theory, as well as from quotient inductive-inductive types.