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.

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