I've seen that there was a single-sorted definition of a category. In some ways, it seems more understandable than the original definition.
I don't know much about category theory. But I would like to know how each definition is useful.
$\begingroup$
$\endgroup$
7
-
21$\begingroup$ The two-sorted definition corresponds to how most people think of categories, and how they talk about categories. For example, we speak of the categories of sets (not of functions), of groups (not of group homomorphisms), of topological spaces (not of continuous maps), etc. (If I remember correctly, Ehresmann did write about the categories of functions, of homomorphisms, of continuous maps, etc., but that never caught on.) $\endgroup$– Andreas BlassCommented Jul 19, 2019 at 16:39
-
1$\begingroup$ One can identify an object with its identity morphism. Then we have a category consisting of morphisms that can be composed. Usually the composition is thought of one function for the whole category. However, the composition function can be broken up into a performing compositions, one such place for each object. In higher order category theory there may be 2-morphisms between the usual morphisms. They may also be places or performing compositions. With the appropriate additional axioms higher order category theory fits into this scheme. $\endgroup$– Jay KangelCommented Jul 19, 2019 at 17:52
-
$\begingroup$ My impression is that the single-sorted POV is slightly more widespread in the context of groupoids (considered as small categories where every morphism is iso) but I am not a specialist and would be happy to be corrected here by others. However, one often ends up introducing the "unit space" of the groupoid which is the "set of objects", so even then two sorts seem to emerge $\endgroup$– Yemon ChoiCommented Jul 19, 2019 at 18:20
-
7$\begingroup$ Another area where the single sorted definition is more widespread is when working with strict $n$-categories or strict $\infty$-categories. Working with the single sorted definition allows to compose arrows of different dimension without writing iterated identities everywhere. It makes the manipulation of expressions a little more bearable, so lots of paper use it (where the "lots" need to be taken relatively as there is not that many paper on that topics anyway) $\endgroup$– Simon HenryCommented Jul 19, 2019 at 19:54
-
4$\begingroup$ Actually I would argue that the homsets-definition (ncatlab.org/nlab/show/category#AFamilyOfCollectionsOfMorphisms) is the one that corresponds to how more people think of categories in practice. $\endgroup$– Mike ShulmanCommented Jul 21, 2019 at 23:26
|
Show 2 more comments
3 Answers
$\begingroup$
$\endgroup$
2
They're so automatically interchangeable that it doesn't really make sense to say that one is more useful than the other except in minor ways: if we really care about "symbolic parsimoy" then the object-free approach has a minor advantage, while if we care about matching informal discourse then objects are generally essential (per Andreas' comment).
Ultimately I'd say that the second point wins out - it's hard to beat intuitive clarity if the cost is so minor. But since the translations in both directions are really so trivial, you can use whichever one you want. And to be fair, it's not the case that the two-sorted approach is always more intuitive - when thinking of a group as a category, having to consider an utterly pointless object is a bit weird at first. (EDIT: Simon Henry's comment points out a more convincing example of this, where the two-sorted approach results in meaningfully annoying technical overhead.)
answered Jul 19, 2019 at 18:48
-
$\begingroup$ So, I would say "to be fair", this is not automatically interchangeable, and rather make sense single-sorted definition is more useful and has major advantages than the two-sorted definition. I really don't understand why people want to advocate the value of "intuitive" thing in this theory of abstraction. I believe many had confusion because of this problem. (including me) $\endgroup$– smith KCommented Aug 30, 2020 at 8:05
-
$\begingroup$ @smithK You can also tell us when single-sorted definition more useful! $\endgroup$ Commented Sep 2, 2022 at 7:24
$\begingroup$
$\endgroup$
Your question is good, as well as the answers. I'm wondering about a first undergraduate course in General Topology, or Measure Theory, or Group Theory, where one would avoid any reference to sets with structures, and everything would be said in terms of morphisms... can you explain even Linear Algebra from scratch with just linear maps and never mention vector spaces nor of course vectors themselves? probably, since a vector in E is the same as a linear map R->E, or in other words, a linear map composable on the right with (the identity of) E and on the left with (the identity of) R. Fun!
$\begingroup$
$\endgroup$
A two-sorted definition is really annoying for certain inductive definitions of a category/families of categories (or maybe an AST representing a category, not yet a category.) In pseudo-Coq
Inductive ast: ast -> ast -> Type :=
| id A: ast A A
| compose A B C: ast B C -> ast A B -> ast A C
(* ... *)
is obviously circular.
Not an expert on these things by any means just ran into these kinds of problems when playing around myself.
answered Apr 4, 2021 at 20:55