This is a continuation of #25 and the discussions in #59 about the notion of a small set and a small category. I want to have this issue focussed on just one property, namely being small. We can generalize later.
The problem
The question is basically: do we want to have the category property of being "small" in the database? Currently, we have it. But being a set or not depends on set theoretic constructions. The proofs that a category is small or not may depend on choices that are completely irrelevant from a category theoretic perspective. Here is a comment by @ykawase5048 from the linked PR:
However, to be honest, I feel a little reluctance about assigning such properties, which are not invariant under isomorphisms. The reason is that, in order to determine whether a category is small, one must fix a set-theoretic construction of that category, but I'm not convinced that such information can always be extracted from the webpage of each category in CatDat. For example, the terminal category is small if its collections of objects and morphisms are constructed as, for example, { ∅ }. But, it might be constructed in a more pathological way, for instance as the functor category [Set,1]. In that case, it would no longer be small.
The underlying issue is that being small (as it is currently defined) is not invariant under isomorphisms.
And that is essentially because a collection which is isomorphic to a set does not have to be a set.
Here is another comment by @ykawase5048 :
As I mentioned in #25, I still believe that the term "essentially small" is confusing. Even though up-to-iso smallness and up-to-equiv smallness coincide for discrete categories, I still think that using "essentially small" for up-to-iso notions goes against the intuition of many category theorists. In particular, when a collection of objects in a category is referred to, category theorists often tend to identify the collection with the full subcategory spanned by those objects. Then, "up-to-iso small" and "up-to-equiv small" are no longer the same concept.
Compromise. It might be better to use "small family" instead in this case. Here, the smallness refers to the index set, so it naturally means up-to-iso smallness. (But, strictly speaking, a family is not the same as a collection, since it allows duplication of elements.)
[...]
Let me take the opportunity to restate my thoughts about smallness here: I still believe that up-to-iso smallness of categories should be included in the database, and that it should share the same name as up-to-iso smallness of sets. However, the term "essentially small" conflicts with the existing notion of up-to-equiv smallness of categories.
Besides, a lot of category theorists who adopt the ZFC+U(universe axiom) as foundation do not distinguish proper smallness and up-to-iso smallness in the text. For example, I usually work in the ZFC+U. When I write "the category of small categories", I means proper smallness; when I write "a small set of objects in a category", I means up-to-iso smallness. I also understand that this convention is not very well-behaved.
Furthermore, it should be emphasized that there is a (non-set-theoretical) foundation where any mathematical object bijective to some small one becomes small. (But, I'm not very familiar with this.)
The "smallness" problem that we are facing might seem weird for those who adopt such a foundation.
We may add "isomorphic to a small category", but: this property apparently has no short name yet? And users maybe be confused by it, since it is never used?
"Essentially small" means "equivalent to a small category". For many aspects of category, this is just as good as being small.
It definitely feels weird that "finite => small" is wrong (with the current definition of "small").
Foundations
The foundations we are (currently) using in CatDat are explained here: https://catdat.app/foundations
Important: In CatDat we should not create just another convention.
This is a continuation of #25 and the discussions in #59 about the notion of a small set and a small category. I want to have this issue focussed on just one property, namely being small. We can generalize later.
The problem
The question is basically: do we want to have the category property of being "small" in the database? Currently, we have it. But being a set or not depends on set theoretic constructions. The proofs that a category is small or not may depend on choices that are completely irrelevant from a category theoretic perspective. Here is a comment by @ykawase5048 from the linked PR:
The underlying issue is that being small (as it is currently defined) is not invariant under isomorphisms.
And that is essentially because a collection which is isomorphic to a set does not have to be a set.
Here is another comment by @ykawase5048 :
We may add "isomorphic to a small category", but: this property apparently has no short name yet? And users maybe be confused by it, since it is never used?
"Essentially small" means "equivalent to a small category". For many aspects of category, this is just as good as being small.
It definitely feels weird that "finite => small" is wrong (with the current definition of "small").
Foundations
The foundations we are (currently) using in CatDat are explained here: https://catdat.app/foundations
Important: In CatDat we should not create just another convention.