Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. 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,

    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.

    • CommentRowNumber2.
    • CommentAuthorvarkor
    • CommentTimeAug 26th 2022

    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).

    • CommentRowNumber3.
    • CommentAuthormaxsnew
    • CommentTimeAug 26th 2022

    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.

    • CommentRowNumber4.
    • CommentAuthorGuest
    • CommentTimeAug 26th 2022

    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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeAug 26th 2022
    • (edited Aug 26th 2022)

    Just a general comment, highlighting what ought to be obvious but maybe is not:

    1. There is no such thing as default definitions on the nLab, nor could there be, given its multi-author nature.

    2. There is no need for entries to make statements only in one tacitly understood particular context, nor would it be desirable.

    3. 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:

        **(category in set theory)** \linebreak
        On a backdrop of [[set theory]]-[[foundations]], a ("strict") category is ....
        **(category in type theory)** \linebreak
        On a backdrop of [[homotopy type theory]]-[[foundations]], one distinguishes...
        **(relation between alternative definitions)** \linebreak
        The above definitions \ref{CategoryInSetTheory} and \ref{CategoryInTypeTheory} are related as follows...
    • CommentRowNumber6.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2022

    One should remember that for NBG or ZFC, the universe VV 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.

    • CommentRowNumber7.
    • CommentAuthorGuest
    • CommentTimeAug 26th 2022

    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.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeAug 29th 2022

    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.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeAug 30th 2022

    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 .