We study the confluence property of abstract rewriting systems internal to cubical categories. We introduce cubical contractions, a higher-dimensional generalisation of reductions to normal forms, and employ them to construct cubical polygraphic resolutions of convergent rewriting systems. Within this categorical framework, we establish cubical proofs of fundamental rewriting results -- Newman's lemma, the Church-Rosser theorem, and Squier's coherence theorem -- via the pasting of cubical coherence cells. We moreover derive, in purely categorical terms, the cube law known from the $λ$-calculus and Garside theory. As a consequence, we show that every convergent abstract rewriting system freely generates an acyclic cubical groupoid, in which higher-dimensional generators can be replaced by degenerate cells beyond dimension two.

翻译：本研究探讨立方体范畴内抽象重写系统的汇合性质。我们引入立方体收缩——一种将约简推广至高维正规形式的高维泛化概念，并运用其构造收敛重写系统的立方体多图分解。在此范畴框架下，我们通过粘贴立方体相干胞腔，建立了基础重写理论结果——纽曼引理、丘奇-罗塞尔定理及斯奎尔相干定理——的立方体证明。此外，我们以纯范畴论术语推导出源于λ演算与加斯德理论中的立方体定律。作为推论，我们证明每个收敛抽象重写系统均可自由生成非循环立方体群胚，其中高维生成元在二维以上可被退化胞腔替代。