Yes, I am likewise concerned. I haven’t had a chance to read the changes carefully, but there are a lot of claims being made in the edit comments that I’m not sure I agree with.
]]>It’s hard to follow the many little edits. But looking over the entry, I am not sure that I see it progressing.
To my mind, the old second paragraph of the Idea-section says it all (I have added links after the word “simplicial set” to make clear that this is already referring to presentation by strict categories):
() For instance, a category can be presented by a simplicial set (the nerve of a corresponding strict category, see there), but isomorphism of simplicial sets is much finer than equivalences of their corresponding categories. It is generally a mistake to mix up these two levels and, for instance, assign to a category properties that are shared only by some of the simplicial sets representing it, say, by distinguishing between isomorphic objects. This breaks the equivalence invariance. (However, see below.)
The last pointer, after “However”, was added recently. It points to a new section at the very, very end – which however really just reiterates this paragraph in different words. This seems chaotic.
Similarly, under “Examples” the first section “In category theory” is yet another rewording of the above paragraph, which means that keeping it under “Examples” and, all the more, prefixing it with the words “A common misconception…”, seems logically wrong.
In contrast, the original version of the paragraph above (from rev 70, in 2012) ended with “This breaks the principle of equivalence.” where “This” was referring to “Mixing up these two levels”.
This was completely correct, and it should not have been deleted.
Notice how the new paragraph beginning with “A common misconception…” (introduced yesterday by “Anonymous”) is itself misconstruing the above paragraph () and is fighting a straw man where it says: “… misconception that strict categories violate the principle of equivalence”. I don’t think anyone said this, much less commonly so. Instead, the second paragraph () already said correctly that it is the “mixing up” of the level of strict categories with the other level that is the breaking of the principle of equivalence, and of course that’s true.
In short, I don’t see that the recent half dozen of Anonymous edits to the entry are advancing its quality.
]]>similarly in the identity-on-objects functor: equality of objects is does not violate this principle; equality of sets is what violates this principle. So removed the paragraphs whuch insisted that strict categories and precategories violate the principle of equivalence.
Anonymous
]]>important for the concrete categories to have nontrivial automorphisms.
Anonymous
]]>edited section on category theory to clarify when exactly the principle of equivalence is violated: it occurs when a category of set-level structures like Set or Grp is said to be strict, because then one is comparing sets for equality.
Anonymous
]]>Incidentally, there is no problem with the 1-category Cat even in a framework where it’s impossible to violate the principle of equivalence; e.g. it is equivalent to a full subcategory of set(oid)-valued presheaves on .
Or maybe more informatively, Cat is equivalent to the full subcategory of (where is the (2,1)-category of 1-categories) consisting of essentially surjective functors whose domain is a set(oid), thus expressing the idea that an object of Cat as a category together with a representative set of points.
]]>problems as set-theoretic based definitions in regards to the principle of equivalence
Am I missing something? AFAICT There is no “problem” with the set-theoretic based definition of categories unless you insist that it is impossible to violate the principle of equivalence. In set-theoretic foundations, a category has a discrete set/class of objects and they can be compared for equality. This is the style that 99% of pages on the nlab are written in so we shouldn’t be rewriting pages to be inconsistent with this without prefacing with them by “this is all in homotopy type theory” or something.
I am all for homotopy-izing mathematics, but the nlab has a ton of material based on set theoretic definitions and it will only confuse users/readers if we mix radically different foundations.
]]>varkor,
My second comment wasn’t about the terminology, it was about how class-theoretic based definitions suffer from the same problems as set-theoretic based definitions in regards to the principle of equivalence. I was busy writing my second comment when you posted your comment, so I didn’t actually see your comment until after I posted my comment and refreshed my page.
Let’s move the discussion about terminology over to the new discussion post I’ve created The default definition of category on the nLab.
]]>Regarding #38: my comment was purely terminological, and only in reference to the previous comments, rather than this article. If a class-theoretic category has undesirable properties, then I can well understand the desire to use a different structure. But the term “category” is already widely established, and I do not believe we should change its meaning on the nLab unless the meaning overwhelming changes in modern literature.
]]>If we define a class in the material set theory sense, as a proposition with a free variable, saying that Set is a locally small category in the class-theoretic sense as in having a class of objects and a set of morphisms still violates the principle of equivalence, because elements of a class still can be compared for equality, which for Set is akin to saying that there is proposition-valued equality between sets.
This is also true if we define a class as an object in a category of classes, since a category of classes is basically a predicative set theory, being a univalent well-pointed Heyting pretopos with a natural numbers object, but without power objects, so suffers from the same problems with the principle of equivalence as saying that Set is a category in structural set theory does.
]]>I am strongly of the opinion that “category” on the nLab should mean what is referred to in Homotopy Type Theory as a “strict category”. This is the by far the most prevalent usage in the literature, and overloading it (or not using it in lieu of “strict category”) will just serve to confuse readers. Since there are explicit terms in HoTT for the other concepts (as mentioned in #36), these terms may be used on the nLab, leaving the term “category” for the set-theoretic definition as is standard.
]]>I disagree with the use of the term “category” for precategories.
“Category” is a nebulous concept in the same way that “space” is in mathematics. It has multiple formal definitions as a strict category, a precategory, or a univalent category, depending upon the author and the foundations, and all three of them behave differently from each other. There are also -truncated precategories, which for coincide with strict categories, and which for still do not coincide with univalent categories: while all univalent categories are 1-truncated, strict categories are 1-truncated but are not univalent. Strict univalent categories also exist. The walking parallel pair is a strict univalent category, as is every poset.
There are models of Martin-Löf type theory (such as homotopy type theory) and cubical type theory (such as Cartesian cubical type theory) where types are untruncated infinity-groupoids, and so precategories are similarly untruncated infinity-groupoids and is actually a univalent (infinity,1)-category. In general, if there is the axiom in the type theory that all types are -truncated, then precategories are also -truncated and is a univalent (n+1,1)-category.
In addition, if we define a class to be a proposition with a free variable, large categories as defined in a set theory with classes or internally in a category of classes (with a class of objects and a family of class of morphisms) are not precategories, but rather the analogue of a wild category in type theory definition-wise (with a type of objects and a family of types of morphisms). The class-theoretic analogue of a precategory in type theory is a locally small category.
]]>heavily modified the section on identity-on-objects functor to highlight the relation between identity-on-object functors, bijective-on-object functors, equivalent-on-object functors, and essentially surjective functors, strict categories, univalent categories, and univalent universes in type theory, and the proper conditions for which an identity-on-object functor does not violate the principle of equivalence: only between univalent categories in a univalent universe.
Anonymous
]]>Definition 5.2 has another name on the nLab: bijective on objects functor.
]]>@32 The HoTT book uses “category” for what the nLab calls univalent category. The categories described in this article are what the HoTT book calls “precategories”. Indeed, the next sentence which follows after your quote is
However, it does carry an appropriate connotation here, because for general precategories, isomorphism is stronger than equivalence.
As a result, using the nLab terminology, while every isomorphism of categories is a identity-of-objects functor, not every equivalence of categories is an identity-of-objects functor.
]]>@30
The HoTT book later has this statement on page 318:
]]>On the other hand, the following characterization of equivalences of categories is perhaps even more useful.
Definition 9.4.8. A functor is an isomorphism of (pre)categories if is fully faithful and is an equivalence of types.
This definition is an exception to our general rule (see §2.4) of only using the word “isomorphism” for sets and set-like objects.
@29 : For the purposes of definitions 5.3 and 5.4, I suspect the intent is not to assume Rezk completeness, so we can’t assume every arrow that is an isomorphism comes from an equivalence of objects.
]]>@29, the HoTT book defines an equivalence of categories to be:
Definition 9.4.1. A functor is an equivalence of (pre)categories if it is a left adjoint for which and are isomorphisms.
is the unit of an adjuncation and is the counit of an adjuncation.
]]>definitions 5.2-5.4 are all wrong in type theory, as they use the wrong notion of ’the same type of objects’. Two types are the same when they are definitionally equal. Using homotopy equivalence and/or identity/path types is not sufficient, as the unit type and interval type are equivalent to each other, but they are not the same type: they are not definitionally equal, and also adding an interval type to a dependent type theory with identity types results in function extensionality being true; adding the unit type does not.
If one wants to say that two categories and have the same type of objects, then has to be definitionally equal to . In foundations without definitional equality, then you only have one collection of objects with two different families of morphisms indexed by the objects. The identity-on-objects ’functor’ isn’t a functor anymore, but just the morphism-preserving functions.
]]>Re #24 : we’re discussing both.
Let be the category with one object and be the category with two objects such that is an equivalence.
Thus, “identity-on-objects functor” does not respect equivalences.
]]>The bigger problem is that the section on identity-on-objects functors assumes that strict categories are inherently evil. They aren’t inherently evil, what is evil is assuming that certain concrete categories like Set and Top and Met are strict categories, because then you are actually comparing sets for equality. The definitions 1.2-1.4 all define perfectly valid functors. The right notion of identity of objects in a strict category is by definition proposition-valued equality, and so the right notion of identity of two sets of objects is bijection. But most of the actual commonly used categories of sets-with-additional-structure like Rel or Hilb are not strict categories.
different guest
]]>Urs Schreiber,
the two definitions are about defining an identity-on-objects functor, rather than an equivalence of categories. The two are of course not the same.
]]>