Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Sorry for asking a stupid question, but is a protocategory essentially the same thing as a category enriched in Set (which doesn’t require disjointness of hom-sets)? If not, can you give a simple example to illustrate the distinction?
I think that’s about right as long as by Set you mean the category of sets in a material set theory. But the definition of protocategory makes sense even in a structural set theory.
Thanks; I think I sorted out my confusion, especially with the help of the example of one category being structured over another, as Grp is structured over Set. In that type of example, some protomorphisms do not name any morphism of the generated category. Whereas in the examples I had in mind of Set-enriched categories, we get a protocategory whose protomorphisms are elements of the union of the hom-sets – but in that type of example every protomorphism names some morphism. (Besides the fact that the operation “taking the union” works a little differently when working over a structural set theory from how it does in a material set theory, as you say – about all we have available in a structural set theory is taking a disjoint union.)
Actually, thinking about it some more, I think it’s not necessarily always true that we can make a protocategory by taking unions of hom-sets, because the composition predicate of a protocategory isn’t parametrized by objects. So if we take unions of homsets, then the only way available to define g∘f=h is that there exists some A,B,C such that f:A→B, g:B→C, h:A→C, and g∘A,B,Cf=h. But consider an example like this:
Then if we take unions of homsets we have g∘f=h and also g∘f=h′, but then the protocategory composition axiom fails: we have f:0→1 and g:1→2, but there does not exist a unique k such that k:0→2 and g∘f=k.
I’ve added this to the entry.
1 to 7 of 7