Higher Globular Catoids and Quantales

Cameron Calk and Georg Struth 📧

January 24, 2024


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.


BSD License


Related publications

  • Calk, C., Goubault, E., Malbos, P., & Struth, G. (2022). Algebraic coherent confluence and higher globular Kleene algebras. Logical Methods in Computer Science, Volume 18, Issue 4. https://doi.org/10.46298/lmcs-18(4:9)2022
  • Calk, C., Malbos, P., Pous, D., & Struth, G. (2023). Higher Catoids, Higher Quantales and their Correspondences (Version 1). arXiv. https://doi.org/10.48550/ARXIV.2307.09253

Session OmegaCatoidsQuantales