一句话：提出拟严格高阶范畴的数据结构，支持4-范畴计算并机器验证了一类伴随提升定理。
传统高阶范畴的代数表示通常具有很高的公理复杂度，导致具体计算困难。本文针对拟严格高阶范畴提出新的数据结构，其中结合律和单位律严格成立，从而以较低的公理复杂度表示高阶结构，并给出在拟严格4-范畴中进行计算的实际方法。该表示适合计算机实现；作者利用这一实现给出了机器验证的代数证明，表明拟严格4-范畴中每个1-胞的伴随都可提升为满足蝶形方程的一致伴随。
We present new data structures for quasistrict higher categories, in which associativity and unit laws hold strictly. Our approach has low axiomatic complexity compared to traditional algebraic approaches, and gives a practical method for performing calculations in quasistrict 4-categories. It is amenable to computer implementation, and we exploit this to give a machine-verified algebraic proof that every adjunction of 1-cells in a quasistrict 4-category can be promoted to a coherent adjunction satisfying the butterfly equations.