  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.
