Catoids, Categories, Groupoids

Georg Struth 📧

August 14, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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).


BSD License


Related publications

  • Cranch, J., Doherty, S., & Struth, G. (2020). Convolution and Concurrency (Version 1). arXiv.
  • 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.
  • Fahrenberg, U., Johansen, C., Struth, G., & ZiemiaĹ„ski, K. (2023). Catoids and modal convolution algebras. Algebra Universalis, 84(2).
  • Calk, C., Malbos, P., Pous, D., & Struth, G. (2023). Higher Catoids, Higher Quantales and their Correspondences (Version 1). arXiv.

Session Catoids