Email Gateway (Aug 16 2023 at 17:20): Email Gateway (Aug 16 2023 at 17:20):From: Gerwin Klein <kleing@unsw.edu.au>
Catoids, Categories, Groupoids
by Georg Struth
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).
[https://www.isa-afp.org/entries/Catoids.html]
Enjoy!
Gerwin
Last updated: Apr 28 2024 at 20:16 UTC