### Abstract

This AFP entry formalises catoids, which are generalisations of single-set categories, and groupoids. More specifically, in catoids, the partial composition of arrows in a category is generalised to a multioperation, which sends pairs of elements to sets of elements, and the definedness condition of arrow composition -- two arrows can be composed if and only the target of the first matches the source of the second -- is relaxed. Beyond a library of basic laws for catoids, single-set categories and groupoids, I formalise the facts that every catoid can be lifted to a modal powerset quantale, that every groupoid can be lifted to a Dedekind quantale and to power set relation algebras, a special case of a famous result of Jónsson and Tarski. Finally, I show that single-set categories are equivalent to a standard axiomatisation of categories based on a set of objects and a set of arrows, and compare catoids with related structures such as multimonoid and relational monoids (monoids in the monoidal category Rel).

### License

BSD License

### Topics

- Mathematics/Algebra
- Mathematics/Category theory

### Related publications

- Cranch, J., Doherty, S., & Struth, G. (2020). Convolution and Concurrency (Version 1). arXiv. https://doi.org/10.48550/ARXIV.2002.02321
- Calk, C., Fahrenberg, U., Johansen, C., Struth, G., & Ziemiański, K. (2021). $$\ell r$$-Multisemigroups, Modal Quantales and the Origin of Locality. Lecture Notes in Computer Science, 90–107. https://doi.org/10.1007/978-3-030-88701-8_6
- Fahrenberg, U., Johansen, C., Struth, G., & Ziemiański, K. (2023). Catoids and modal convolution algebras. Algebra Universalis, 84(2). https://doi.org/10.1007/s00012-023-00805-9
- 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 Catoids

- Catoid
- Groupoid
- Catoid_Lifting
- Groupoid_Lifting
- Multimonoid

### Depends on

- Kleene Algebras with Domain
- Quantales
- Modal quantales, involutive quantales, Dedekind Quantales
- Relation Algebra

### Used by

- Cubical Categories
- Higher Globular Catoids and Quantales

## Cite

×

Catoids-AFP

    @article{Catoids-AFP,
      author  = {Georg Struth},
      title   = {Catoids, Categories, Groupoids},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Catoids.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Aug 16, 2023 : Isabelle2022