Catoids, Categories, Groupoids

Georg Struth 📧

August 14, 2023


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

Session Catoids