This article is part of a programme on the formalisation of higher categories and the categorification of rewriting theory. Set-valued structures such as catoids are used in this context to formalise local categorical composition operations. We introduce omega-catoids as set-valued generalisations of (strict) omega-categories. We establish modal correspondences between omega-catoids and convolution omega-quantales. These are related to J\'onsson-Tarski-style dualities between relational structures and lattices with operators. Convolution omega-quantales generalise the powerset omega-Kleene algebras recently proposed for algebraic coherence proofs in higher rewriting to weighted variants in the style of category algebras. In order to capture homotopic constructions and proofs in rewriting theory, we extend these correspondances to higher catoids with a groupoid structure above some dimension, which is reflected by an involution in higher quantales.

翻译：本文是高阶范畴形式化与重写理论范畴化研究计划的一部分。在此背景下，我们使用如范畴体（catoids）这类集合值结构来形式化局部范畴复合操作。我们引入omega-范畴体作为（严格）omega-范畴的集合值推广，并建立了omega-范畴体与卷积omega-量子之间的模态对应关系。这些关系与约恩松-塔斯基风格的 relational 结构与带算子格之间的对偶性相关联。卷积omega-量子将近期为高重重写代数一致性证明提出的幂集omega-克莱因代数，推广至范畴代数风格的加权形式。为捕捉重写理论中的同伦构造与证明，我们将这些对应关系扩展到具有高于某维度的群胚结构的高阶范畴体上，这种结构在高阶量子中通过对合操作体现。