### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Category theory
- Mathematics/Algebra

### 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 2). arXiv. https://doi.org/10.48550/ARXIV.2307.09253

### Session OmegaCatoidsQuantales

- Two_Catoid
- Two_Kleene_Algebra
- Two_Quantale
- Two_Catoid_Lifting
- Two_Catoid_Collapse
- Omega_Catoid
- Omega_Kleene_Algebra
- Omega_Quantale
- Omega_Catoid_Lifting

### Depends on

- Catoids, Categories, Groupoids

### Auto-related entries

- Cubical Categories
- Go Code Generation for Isabelle
- Zermelo Fraenkel Set Theory in Higher-Order Logic
- Quaternions
- Type Constructor Classes and Monad Transformers

## Cite

×

OmegaCatoidsQuantales-AFP

    @article{OmegaCatoidsQuantales-AFP,
      author  = {Cameron Calk and Georg Struth},
      title   = {Higher Globular Catoids and Quantales},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/OmegaCatoidsQuantales.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest