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