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

nLab > Latest Changes: principle of equivalence

Bottom of Page

1 to 47 of 47

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 8th 2012
    • (edited Sep 8th 2012)

    at principle of equivalence I have restructured the Examples-section: added new subsections in “In physics” on gauge transformations and on general covariance (just pointers so far, no text), and then I moved the section that used to be called “In quantum mechanics” to “Examples-In category theory” and renamed it to “In the definition of †\dagger-categories” (for that is really what these paragraphs discuss, not any notion of equivalence in quantum mechanics, the application of †\dagger-categories in that context notwithstanding)

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeSep 8th 2012
    • (edited Sep 8th 2012)

    And I move the “How to break equivalence-invariance” to the end. At least it should go after the “General definition”, I’d say.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 9th 2012

    So general covariance is an example of the (mathematical) principle of equivalence. Remind me, how should I think of the (physical) principle of equivalence? I think somewhere you just said it’s a result of using Riemannian spaces. So the physical principle of equivalence is part of a precondition for the mathematical principle of equivalence to have as special case general covariance?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 9th 2012
    • (edited Sep 9th 2012)

    Remind me, how should I think of the (physical) principle of equivalence?

    I am claiming that the mathematical formalization of the “principle ofequivalence” in the theory of gravity is (or was, in the time when people actually referred to it):

    1. the infinitesimal neighbourhood of every point in spacetime is a vector space (the tangent space);

    2. the Levi-Civita connection can be taken (up to its gauge freedom) to vanish on that neighbourhood (not it’s derivative, though, hence not the curvature). This is the existence of “Riemann normal coordinates”.

    In conclusion: in first order approximation around any point, gravitational dynamics looks like dynamics in flat space.

    So that “principle of equivalence” is not so very close to the mathematical “principle of equivalence” as we have on that page. What we have on the page principle of equivalence however directly subsumes what in gravity is the principle of general covariance.

    But of course the relation is via those Riemann normal coordinates (or can be understood that way): the principle of general covariance says that if you see a field of gravity gg on spacetime Σ\Sigma, you may regard it as being equivalent to the field of gravity g˜≔f *g\tilde g \coloneqq f^* g for any diffeomorphism f:Σ→Σf : \Sigma \to \Sigma. The statement of Riemann normal coordinates is that you can always find such a diffeomorphism such that at a given point f *gf^* g induces vanishing Levi-Civita connection at that point, hence proving that up to gauge equivalence the dynamics in the infinitesimal neighbourhood of that point is that of flat space.

    That’s how these things relate. Schematically we have implications

    principle of equivalence in mathematics ⇒\Rightarrow principle of general covariance ⇒\Rightarrow principle of equivalence in physics

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 9th 2012

    I turned this into a quick note here. But need to quit now.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 7th 2018

    One day we should probably extract some text from that discussion at In the concept of †-categories. But for now, I added a link to this old MO discussion – Are dagger categories truly evil?.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 15th 2018

    Added a reference

    diff, v90, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMar 24th 2021

    Touched the lead-in sentences, adding more hyperlinks (such as to higher structures).

    Removed two more pointless appearances of the word “evil”.

    diff, v93, current

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 24th 2021

    I wonder if that long discussion on dagger categories could be condensed and extracted now with the benefit of hindsight.

    • CommentRowNumber10.
    • CommentAuthorKeith Harbaugh
    • CommentTimeMar 28th 2021

    Updated inline link to: Makkai 1995 “Towards a Categorical Foundation of Mathematicics”

    diff, v94, current

    • CommentRowNumber11.
    • CommentAuthorGuest
    • CommentTimeMar 12th 2022
    This page says "It does not break equivalence-invariance to state that two morphisms are equal, given a common source and target; this is because a hom-set is a set, where equality is meaningful." But if I click on the "hom-set" link, it says that a hom-set is only a set for a locally small category. Does this matter?

    I think that maybe this claim and the corresponding claim in the next paragraph should be removed.
    • CommentRowNumber12.
    • CommentAuthorGuest
    • CommentTimeMar 12th 2022
    that's probably because hom-sets are large (i.e. classes) in a large category, and so aren't small (i.e. set).
    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMar 12th 2022

    Yes, but size issues are not the point here, the point is the uniqueness of identities between elements, the choice of ambient universe does not change this. Of course it won’t hurt to add further clarifying remarks, if this seems confusing. But for that we first need to have the edit functionality back.

    • CommentRowNumber14.
    • CommentAuthorGuest
    • CommentTimeMar 12th 2022
    Is there a difference between "size issues," i.e. whether or not a collection of objects is too large to be a set, and the issue of whether the objects can be meaningfully compared for equality?
    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2022

    Yes, they’re entirely unrelated questions. A small collection can lack a strict equality, while a large collection can have one.

    • CommentRowNumber16.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 14th 2022

    that’s probably because hom-sets are large (i.e. classes) in a large category, and so aren’t small (i.e. set).

    I’d like to push back against this: a large category can have small homs, eg the category of sets.

    The category of classes (of NBG classes, for example) is not locally small, and given two class functions between the same pair of classes, we can define their equaliser, and then ask if the equaliser is inhabited. This is a proposition of first-order logic.

    • CommentRowNumber17.
    • CommentAuthorGuest
    • CommentTimeJul 26th 2022
    There's a query box on this page
    • CommentRowNumber18.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 26th 2022

    Moving query box to here.

    This definition break equivalence-invariance: it imposes equations between objects, so we cannot transport a dagger-category structure along an equivalence of categories. Often concepts violating the principle of equivalence (like the concept of “strict monoidal category”) have equivalence-invariant counterparts (like the concept of “monoidal category”). But in this particular case there appears to be no known way to express the idea without equations between objects. Both Hilb and nCob are dagger-categories. This fact is important. Try saying it in a way that obeys the principle of equivalence!

    It is possible that this problem will force a change in thinking in either the concept of the principle of equivalence or our thinking in quantum theory.

    See also the MO discussion – Are dagger categories truly evil?.

    Mike Shulman: Actually, I believe that †\dagger-structure on a category can be transported along an equivalence of categories! Suppose that F:C→D:GF\colon C \to D \colon G is an adjoint equivalence with unit η:Id C→≅GF\eta\colon Id_C \overset{\cong}{\to} G F and counit ε:FG→≅Id D\varepsilon\colon F G \overset{\cong}{\to} Id_D, where DD is a †\dagger-category. Given f:x→yf\colon x\to y in CC, define f †f^\dagger to be the following composite:

    y→ηGFy→G((Ff) †)GFx→η −1x. y \overset{\eta}{\to} G F y \overset{G((F f)^\dagger)}{\to} G F x \overset{\eta^{-1}}{\to} x.

    This evidently defines a functor C op→CC^{op} \to C that is the identity on objects. Now F(f †)F(f^\dagger) is given by

    Fy→FηFGFy→FG((Ff) †)FGFx→Fη −1Fx F y \overset{F \eta}{\to} F G F y \overset{F G((F f)^\dagger)}{\to} F G F x \overset{F \eta^{-1}}{\to} F x

    but by the triangle identities this is equal to

    Fy→ε F −1FGFy→FG((Ff) †)FGFx→ε FFx F y \overset{\varepsilon^{-1}_F}{\to} F G F y \overset{F G((F f)^\dagger)}{\to} F G F x \overset{\varepsilon_F}{\to} F x

    and hence equal to (Ff) †(F f)^\dagger by naturality of ε\varepsilon. Thus, since ((Ff) †) †=Ff((F f)^\dagger)^\dagger = F f in DD, in CC we have that (f †) †(f^\dagger)^\dagger is given by

    x→ηGFx→GFfGFy→η −1y. x \overset{\eta}{\to} G F x \overset{G F f}{\to} G F y \overset{\eta^{-1}}{\to} y.

    which is equal to ff by naturality of η\eta. Thus, CC is a †\dagger-category, and essentially by construction FF and GG are †\dagger-functors (though η\eta and ε\varepsilon need not be unitary).

    So if a notion refers to equality of objects in a seemingly irreducible way, but it can nevertheless be transported along an equivalence of categories, does it break equivalence invariance or not? Thinking about it some more, I’m actually not convinced that †\dagger-structure violates the principle of equivalence at all. Consider the assertion that a category is a groupoid. Clearly this does not break equivalence-invariance! But what it means is that for any morphism f:x→yf\colon x\to y, there exists a morphism f −1:y→xf^{-1}\colon y\to x whose source is equal to the target of ff, and whose target is equal to the source of ff, and such that ff −1f f^{-1} and f −1ff^{-1} f are identities. The notion of †\dagger-category is entirely analogous: for any morphism f:x→yf\colon x\to y, we are given a specified morphism f †:y→xf^\dagger\colon y\to x with certain properties. The only difference is that the first is a property and the second is structure, but why should that matter?

    As remarked in the discussion below, equality of objects is all over the place in category theory: whenever we introduce an arrow, we have to say what its source and target are, and one or the other (or both) will often be equal to some object we are already considering. But this does not really break equivalence-invariance; it’s really just a typing assertion. (If you write category theory in a logic of dependent types like FOLDS, then that’s exactly what it is.) Maybe †\dagger-structure is just the same.

    Mike Shulman: Here’s an interesting analogy: let GG be a group and consider categories enriched over GG-sets. In such a category, for every morphism f:x→yf\colon x\to y and every g∈Gg\in G we have another morphism f g:x→yf^g\colon x\to y satisfying certain axioms, which may look like breaking equivalence-invariance (since f gf^g has equal source and target to ff) but is really not. Moreover, just like for †\dagger-categories and unitary isomorphisms, in this case the “underlying groupoid” is not the naive core of the original category, but consists of only the GG-fixed isomorphisms. Actually, †\dagger-categories have always felt a lot like enriched categories to me, though the “enrichment” is sort of “non-local” in that the structure on homsets relates more than one of them, so it’s hard to make this precise.

    Toby: I agree, the concept is not really violating the principle of equivalence, although you have clarified the ideas for me, so that now I think that I can write a good note to the mailing list. (In particular, the idea that a dagger structure is analogous to the property of being a groupoid, only slightly harder to grok since it is not a property-like structure, was helpful.)

    If you specify a functor †:C op→C\dagger\colon C^{op} \to C and ask whether it is a dagger structure, that is (taken literally) a question that breaks equivalence-invariance; you can ask instead whether it is naturall isomorphic to a dagger structure. But the concept of dagger structure does not itself violate the principle of equivalence, if broken down a little.

    Peter Selinger: what you have shown here is a special case of the fact that dagger structure is reflected by full and faithful functors. Specifically, given F:C→DF\colon C\to D full and faithful, and a dagger structure on DD, you can define a dagger structure on CC by the equation F(f †)=(F(f)) †F(f^\dagger) = (F(f))^\dagger. This obviously uniquely determines f †f^\dagger, because FF is full and faithful. It is also the unique dagger structure on CC such that FF becomes a dagger functor. It’s almost trivial to verify that this is indeed a dagger structure.

    It coincides with what Mike Shulman has defined, showing in particular that his definition is independent of GG, η\eta, and ε\epsilon. Moreover, the definition is not invariant under natural isomorphism of FF; given a different F′F' naturally isomorphic to FF, this will in general induce a different dagger structure on CC. Also, GG will not be a dagger functor with respect to the structure Mike defined.

    To me, the facts listed in the last paragraph are good indication that Mike’s notion is not the right notion of “transporting structure along an equivalence”. I would expect both FF and GG to respect the transported structure. I would even go as far as requiring η\eta and ε\epsilon to be dagger natural transformations w.r.t. the transported structure. (A dagger natural transformation is one that is componentwise unitary).

    I proposed a formal definition of “transporting structure along an equivalence” on the categories list. It works for any 2-functor between 2-categories.

    Peter Selinger: Here is another view of dagger categories. What makes some people uneasy about the dagger structure is that it runs counter to the usual categorical intuition that all information is contained in the morphisms. Or more precisely, that all information about an object AA is contained in the natural family of hom-sets (X,A)(X,A). So in ordinary category theory, we consider two objects AA, BB “the same” if they have “the same” generalized points, i.e., if the contravariant representable functors (X,A)(X,A) and (X,B)(X,B) are naturally isomorpic.

    (X,A)→nat.isomorphism(X,B) (X,A) \overset{nat.\;isomorphism}\to (X,B)

    Alternatively, one can say that AA and BB are the same if the covariant representable functors are naturally isomorphic.

    (A,X)→nat.isomorphism(B,X) (A,X) \overset{nat.\;isomorphism}\to (B,X)

    Of course, by the Yoneda Lemma, both conditions are equivalent to an isomorphism between AA and BB, and therefore to each other. But that is just a lucky simplification.

    In dagger categories, the hom-sets are also equipped with distinguished bijections †:(X,A)→(A,X)\dagger\colon(X,A)\to (A,X). It therefore makes sense to say that, for two objects to be “really” the same, not only should one have natural isomorphisms such as above, but further that the diagram should commute:

    (X,A) →nat.isomorphism (X,B) †↓ ↓† (A,X) →nat.isomorphism (B,X) \array { (X,A) & \overset{nat.\;isomorphism}\to & (X,B) \\ \dagger \downarrow & & \downarrow \dagger \\ (A,X) & \overset{nat.\;isomorphism}\to & (B,X) }

    In general, an isomorphism f:A→Bf \colon A \to B will induce natural isomorphisms (X,A)→(X,B)(X,A) \to (X,B) and (A,X)→(B,X)(A,X) \to (B,X) that do not make the diagram commute. It makes the diagram commute if and only if for all g∈(X,A)g\in(X,A), g †∘f −1=(f∘g) †g^\dagger \circ f^{-1} = (f \circ g)^\dagger, in other words, if and only if ff is unitary. This is why unitary isomorphisms are the “real” isomorphisms of dagger categories, and unitary natural transformations are the “real” natural transformations of dagger categories. They preserve and transport everything.

    All this indicates to me that dagger is a primitive operation (like composition). In this respect I completely agree with Toby. As a primitive operation, dagger must be included in the definition of primitive concepts, such as equivalence. And primitive operations (like composition) are allowed to talk about objects and be strict.

    If someone knows how to wiki-ize the above diagrams, please feel free.

    Toby: I did the diagrams a bit, but I don't have any more time for a complete reply tonight.

    Mike Shulman: Okay, you are right. “Transporting along an equivalence” should mean that the forgetful functor is an equiv-fibration, i.e. lifts entire adjoint equivalences rather than merely functors that happen to be equivalences. I think I disagree, however, that primitive operations (in something that we want to think of as a kind of category theory) should be freely allowed to talk about objects and be strict; I think they should also be formulated in a dependent type theory that only uses equality of objects as a typing assertion. Dagger categories also satisfy this property.

    diff, v97, current

    • CommentRowNumber19.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 26th 2022

    Linked to archived discussion on the nForum (in previous comment).

    diff, v97, current

  20. adding a section on identity-on-objects functors

    Anonymous

    diff, v98, current

    • CommentRowNumber21.
    • CommentAuthorGuest
    • CommentTimeAug 23rd 2022

    The article, similar to the identity-on-objects functor article, states

    However, both these definitions still nevertheless violate the principle of equivalence, for the same reason that the translation of the usual definition of a Grothendieck fibration or strict creation of limits into type theory violates the principle of equivalence

    How does definition 1.3 (and definition 1.4 which assumes univalence) violate the principle of equivalence? Unlike the case for Grothendieck fibrations, it doesn’t talk about equality of objects at all. Regarding definition 1.4: this article also states towards the beginning

    A very precise way of stating this idea is encapsulated in Vladimir Voevodsky‘s univalence axiom, which is a fundamental part of homotopy type theory as a foundation for mathematics. By identifying equivalences/isomorphisms with inhabitants of an identity type, it ensures that all properties and structure which can be expressed within the formal type theory are invariant under such

    • CommentRowNumber22.
    • CommentAuthorGuest
    • CommentTimeAug 23rd 2022
    *definitions 5.3 and 5.4 in this article
    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeAug 23rd 2022

    How does definition 1.3 (and definition 1.4 which assumes univalence) violate the principle of equivalence? Unlike the case for Grothendieck fibrations, it doesn’t talk about equality of objects at all.

    Because an equivalence of categories need not be an equivalence on their type of objects. That’s essentially the one main point that this entry is or ought to be about. If that point is lost, maybe the entry needs a complete rewrite.

    • CommentRowNumber24.
    • CommentAuthorGuest
    • CommentTimeAug 23rd 2022

    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.

    • CommentRowNumber25.
    • CommentAuthorGuest
    • CommentTimeAug 23rd 2022

    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

    • CommentRowNumber26.
    • CommentAuthorHurkyl
    • CommentTimeAug 23rd 2022
    • (edited Aug 23rd 2022)

    Re #24 : we’re discussing both.

    Let AA be the category with one object and BB be the category with two objects such that p:B→Ap : B \to A is an equivalence.

    • id:A→Aid : A \to A is an identity-on-objects functor
    • p:B→Ap : B \to A is an equivalence
    • applying the equvialence pp to the first copy of AA in the first point above results in the proposition “id∘p:B→Aid \circ p : B \to A is an identity-on-objects functor”
    • but that proposition is false.

    Thus, “identity-on-objects functor” does not respect equivalences.

    • CommentRowNumber27.
    • CommentAuthorGuest
    • CommentTimeAug 23rd 2022
    Urs,

    I don't think that section mentioned your point at all, it seems to have just been copied wholesale from the article on identity-of-objects functor, which contains a message at the end that the section needs more explaining why this was the case.

    Quentin
    • CommentRowNumber28.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

    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 AA and BB have the same type of objects, then Ob(A)Ob(A) has to be definitionally equal to Ob(B)Ob(B). 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.

    • CommentRowNumber29.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022
    According to definition 5.2, every isomorphism of strict categories is an identity-on-objects functor. According to definition 5.3 and 5.4, every equivalence of categories is an identity-on-objects functor
    • CommentRowNumber30.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

    @29, the HoTT book defines an equivalence of categories to be:

    Definition 9.4.1. A functor F:A→BF : A \to B is an equivalence of (pre)categories if it is a left adjoint for which η\eta and ε\epsilon are isomorphisms.

    η\eta is the unit of an adjuncation and ε\epsilon is the counit of an adjuncation.

    • CommentRowNumber31.
    • CommentAuthorHurkyl
    • CommentTimeAug 24th 2022
    • (edited Aug 24th 2022)

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

    • CommentRowNumber32.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

    @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 F:A→BF : A \to B is an isomorphism of (pre)categories if FF is fully faithful and F0:A0→B0F0 : A0 \to B0 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.

    • CommentRowNumber33.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

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

    • CommentRowNumber34.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

    Definition 5.2 has another name on the nLab: bijective on objects functor.

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

    diff, v101, current

  36. 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 nn-truncated precategories, which for n=0n = 0 coincide with strict categories, and which for n=1n = 1 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 PreCatPreCat is actually a univalent (infinity,1)-category. In general, if there is the axiom in the type theory that all types are nn-truncated, then precategories are also nn-truncated and PreCatPreCat 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.

    • CommentRowNumber37.
    • CommentAuthorvarkor
    • CommentTimeAug 26th 2022

    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.

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

    • CommentRowNumber39.
    • CommentAuthorvarkor
    • CommentTimeAug 26th 2022

    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.

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

    • CommentRowNumber41.
    • CommentAuthormaxsnew
    • CommentTimeAug 26th 2022

    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.

    • CommentRowNumber42.
    • CommentAuthorHurkyl
    • CommentTimeAug 26th 2022

    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 Δ\mathbf{\Delta}.

    Or maybe more informatively, Cat is equivalent to the full subcategory of 1Cat [1]1Cat^{[1]} (where 1Cat1Cat 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.

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

    diff, v102, current

  44. important for the concrete categories to have nontrivial automorphisms.

    Anonymous

    diff, v102, current

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

    diff, v103, current

    • CommentRowNumber46.
    • CommentAuthorUrs
    • CommentTimeAug 27th 2022
    • (edited Aug 27th 2022)

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

    (*\ast) 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 (*\ast) 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 (*\ast) 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.

    • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTimeAug 29th 2022

    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.

1 to 47 of 47

  1.