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.
1 to 9 of 9
The nLab currently defines a category to consist of a collection of objects and a collection of morphisms. In the context of class theory, this is a large category, and in the context of type theory, this is a wild category.
Now, over on the discussion page for dagger category:
an anonymous Guest said that the definition of the category should be by default consist of a collection of objects and a set of morphisms, which in the context of class theory is a locally small category and in the context of type theory is a precategory.
and over on the discussion page for principle of equivalence,
https://nforum.ncatlab.org/discussion/4201/principle-of-equivalence/
varkor said that the definition of a category should be by default consist of a set of objects and a set of morphisms, which in the context of class theory is a small category and in the context of type theory a strict category.
Which definition should be the default definition of category used on the nLab? All three definitions of a category represent distinct objects in most other foundations, except for set theory, where they by definition coincide.
To clarify, I think “category” should be taken by default to refer to a large category (if “strict category” means “small category”, then some of the recent anonymous edits are misleading, because they restrict some concepts to sets rather than classes unnecessarily).
When the page category was written, “collection” was not linked to the page collection and it is my impression the author simply wanted to avoid discussing size issues. Size issues (e.g. sets vs classes, or universes) are of a rather different flavour to larger foundational questions such as “sets vs types”. I do not think a wild category can, in general, be called a “category”, just as an internal category would not be referred to in the literature as a category: they are both generalisations, and I do not think it helpful to overload “category” to mean any of these generalisations (especially when there are competing choices).
I think by default on the nlab, category should be viewed with typical ambiguity/”universe polymorphism” in mind, and more precise terms like large/small/locally small used to clarify in specific situations where it’s relevant, like talking about presheaves/having all small limits etc. But for something like a cartesian product of two objects there is no reason to fix the sizes of the categories in mind.
Another problem here is that the term “class” is overloaded.
Is it a large set, as implied by the current category article, with relevance to size issues (i.e. universe enlargement), or is it a formula in the language of set theory for a truth value, equipped with a specified free variable for a set? Classes as formulae behave differently from sets (in particular, one cannot form power classes), and aren’t really relevant to size issues/set-theoretic universes.
Just a general comment, highlighting what ought to be obvious but maybe is not:
There is no such thing as default definitions on the nLab, nor could there be, given its multi-author nature.
There is no need for entries to make statements only in one tacitly understood particular context, nor would it be desirable.
Therefore, where the reader should beware of possible alternative meanings/definitions: make them all explicit!
Use \begin{remark} .. \end{remark}-environments for this purpose.
Or use a list of \begin{definiton} ... \end{definition}-environments and given them discernible names.
For example:
\begin{definition}
\label{CategoryInSetTheory}
**(category in set theory)** \linebreak
On a backdrop of [[set theory]]-[[foundations]], a ("strict") category is ....
\end{definition}
\begin{definition}
\label{CategoryInTypeTheory}
**(category in type theory)** \linebreak
On a backdrop of [[homotopy type theory]]-[[foundations]], one distinguishes...
\end{definition}
\begin{remark}
\label{ComparingCategoryInSetTheoryAndInTypeTheory}
**(relation between alternative definitions)** \linebreak
The above definitions \ref{CategoryInSetTheory} and \ref{CategoryInTypeTheory} are related as follows...
\end{remark}
One should remember that for NBG or ZFC, the universe contains all other classes as subclasses. So we are in a kind of setting parallel to the much more mundane one in structural set theory where one can eg intersect subsets of a given set, but not arbitrary pairs of sets. The universal object in Algebraic Set Theory is similar, in the non-material approach. So there is inherently more structure, when working in that foundation.
There’s a tendency here from some people to use type theory to refer only to some flavor of univalent type theory or homotopy type theory, and talk about mathematics in only that context.
On one hand, it’s not just type theory that has problems with getting the right definition of category (regarding strict category vs precategory vs wild category vs univalent category).
One could also work inside a theory defined in first order logic with dependent sorts (FOLDS), consisting of groupoids, functors between groupoids, natural isomorphisms of functors, and propositional equality of natural isomorphisms, and with appropriate axioms defining the well-pointed elementary (2,1)-topos Grpd.
And one has the same question of whether to use general groupoids or discrete groupoids in the definition of category, and whether there should be a Rezk completion condition for the definition of the category whose object groupoid is not necessarily discrete.
And on the other hand, there are plenty of type theories (such as observational type theory (OTT) or extensional cubical type theory (XTT)) where the types model sets and trying to define a category in that type theory would only ever result in a strict category.
In the vast majority of entries, there is no need to be explicit about foundations, and I think we should not be. Occasionally it is necessary to distinguish between “large” and “small” categories, but this can be done with those well-known words (and links to their pages) and thus in a foundation-agnostic way. The average nLab reader looking at pages about category theory should not encounter any discussions about set theory vs type theory unless they go looking for them. Only in a small number of instances does it matter, and in that case each individual entry can be explicit about its foundations.
However, it’s true that the definitions on our page category are all set-oriented. We should add at least a link to precategory / univalent category, and maybe a bit of discussion .
1 to 9 of 9