Email Gateway (Feb 01 2024 at 07:30): Email Gateway (Feb 01 2024 at 07:30):From: Tobias Nipkow <nipkow@in.tum.de>
Higher Globular Catoids and Quantales
Cameron Calk and Georg Struth
We formalise strict 2-catoids, 2-categories, 2-Kleene algebras and 2-quantales,
as well as their omega-variants. Due to strictness, the cells of these higher
categories have globular shape. We use a single-set approach, generalised to
catoids and based on type classes. The higher Kleene algebras and quantales
introduced extend features of modal and concurrent Kleene algebras and
quantales. They arise for instance as powerset extensions of higher catoids, and
have been used in algebraic confluence proofs in higher-dimensional rewriting.
Details are described in two companion articles.
https://www.isa-afp.org/entries/OmegaCatoidsQuantales.html
Enjoy!
Last updated: Apr 29 2024 at 04:18 UTC