You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Leopold Schlicht (May 01 2021 at 18:48):The principle of equivalence advocates (among other things) to avoid talking about equality between objects of a category. For instance, mostly the notion of equivalence between categories is more useful than the notion of isomorphism between categories, because the latter demands a strict bijection between the classes of objects, while the former only demands a bijection between the isomorphism classes of objects.
The nLab has material about this principle of equivalence and breaking this principle is often referred to as being evil.
I'm wondering why considering (strict) 2-categories and proving coherence theorems like "every bicategory is biequivalent to a 2-category" isn't evil. After all, when checking whether a bicategory is strict (i.e., a "2-category"), one needs (e.g., in the axiom of associativity of composition) to verify that two 1-cells are equal. And 1-cells are just objects of a hom-category, so here one talks about equality of objects.
One justification could be: one defines "category" ("bicategory") in such a way that the class of objects (1-cells) explicitly comes equipped with an equivalence relation that is then called "equality". In this way, talking about 2-categories and coherence theorems doesn't break the principle of equivalence, while stating for example "Cat is a 2-category" does.
Somehow this answer doesn't satisfy me completely. If one is just interested in the notion of a bicategory that doesn't come equipped with an equality relation, why should one nevertheless study bicategories that are equipped with an equality relation? Does this help with studying bicategories without equality at all? Note that then "every bicategory is biequivalent to a 2-category" isn't even a meaningful statement.
Can one motivate coherence theorems for structuralists only interested in bicategories without equality?
John Baez (May 01 2021 at 23:19):I'm wondering why considering (strict) 2-categories and proving coherence theorems like "every bicategory is biequivalent to a 2-category" isn't evil.
It's evil. But sometimes it pays to be evil. :smiling_devil:
Mike Shulman (May 01 2021 at 23:42):This sort of thing is one reason we got rid of the term "evil".
Mike Shulman (May 01 2021 at 23:43):Strictification theorems are, almost by definition, not equivalence-invariant. They are nevertheless extraordinarily useful. However, there are times when one has to work totally invariantly, and then such strictification theorems are not available.
Mike Shulman (May 01 2021 at 23:45):Note though that not every coherence theorem is, or gives rise to, a strictification theorem, and these more general kinds of coherence theorems can still be useful in an equivalence-invariant context.
John Baez (May 02 2021 at 00:42):By the way, I personally never got rid of the term "evil". Jim Dolan always meant it to be humorous. It's not intended to indicate a blanket prohibition, just an important issue to be be aware of.
Mike Shulman (May 02 2021 at 05:01):Sorry; by "we" I meant the nLab.
Mike Shulman (May 02 2021 at 05:01):Which is, of course, not a monolithic entity, and even among the people participating actively in the discussion there were varying viewpoints.
Mike Shulman (May 02 2021 at 05:02):So I should have been more precise.
Oscar Cunningham (May 02 2021 at 06:29):Can't you study strict 2-categories in a nonevil way? Define the weak 3-category of strict 2-categories in such a way that nonisomorphic strict 2-categories are not equivalent. Then there's some functor from this weak 3-category to the weak 3-category of weak 2-categories, and the strictification theorem says that it's essentially surjective on objects.
Oscar Cunningham (May 02 2021 at 06:32):In other words strict 2-categories are different from good (i.e. weak) 2-categories. So although it's evil to talk about equality between objects of 2-categories, it's not evil to talk about equality of objects of strict 2-categories.
Mike Shulman (May 02 2021 at 15:00):You can ask the same question one dimension down, with the 2-category of categories (in which the natural notion of sameness is equivalence) admitting a functor from the 1-category of strict categories (in which the natural notion of sameness is isomorphism), and expecting a strictification theorem that says this functor is essentially surjective. Of course we don't usually think about that version, since in set-theoretic foundations every category comes with a default structure of strict category already.
Mike Shulman (May 02 2021 at 15:03):But in a foundational system where the question is nontrivial, such as homotopy type theory, which mandates the principle of equivalence through the univalence axiom, it turns out that these functors are not essentially surjective. (More precisely, their essential surjectivity is an extra axiom that doesn't follow from the basic theory, and doesn't hold in all models of interest.) So you can certainly study strict categories and strict 2-categories in HoTT, but they are much less interesting than in set-theoretic foundations, because you don't have a strictification theorem.
Mike Shulman (May 02 2021 at 15:08):In other words, it's true that you can talk about strict 2-categories on their own without violating the principle of equivalence; it's the strictification theorem that allows you to then deduce things about weak 2-categories that's dubious.
Leopold Schlicht (May 02 2021 at 18:44):Thanks for all the answers! If structural foundations don't admit strictification theorems offhand, isn't this an argument for material set-theories?
Although I'm not sure whether this issue also applies to structural foundations other than HoTT. If it does, I'm somewhat confused: a recent discussion on MO (https://mathoverflow.net/q/388731) came to the conclusion that every structural statement with a material proof also has a structural proof, roughly speaking. In this way, my naive expectation would be that each application of "evil" techniques such as strictification theorems should be eliminable.
Mike Shulman (May 02 2021 at 19:01):Leopold Schlicht said:
Thanks for all the answers! If structural foundations don't admit strictification theorems offhand, isn't this an argument for material set-theories?
No, it's an argument against strictification theorems. (-:O
Mike Shulman (May 02 2021 at 19:04):Although I'm not sure whether this issue also applies to structural foundations other than HoTT. If it does, I'm somewhat confused: a recent discussion on MO (https://mathoverflow.net/q/388731) came to the conclusion that every structural statement with a material proof also has a structural proof, roughly speaking.
The discussion there was about ETCS, but it applies also to the set-fragment of HoTT. But statements about large categories are not in "the language of ETCS" in this sense, and similarly the relevant categories we're talking about don't live in the set-fragment of HoTT.
Mike Shulman (May 02 2021 at 19:04):(The question isn't really about size but about categorical dimension, but the most natural examples of non-strict categories are large, like the category of sets.)
Mike Shulman (May 02 2021 at 19:07):(Also, ETCS doesn't really have a good way to talk about large categories at all, so it's hard to make the question precise there.)
Fawzi Hreiki (May 02 2021 at 19:29):Mike Shulman said:
(Also, ETCS doesn't really have a good way to talk about large categories at all, so it's hard to make the question precise there.)
How about a boolean category (or pretopos maybe) with a model of ETCS internally? I guess this is in the vein of algebraic set theory.
Mike Shulman (May 03 2021 at 00:06):Yes, you can work in a structural version of a class-set theory, or just assume there are category-theoretic universes inside your model of ETCS. In that case strictification works just as well as it does in ZFC. Same if you work in type theory with UIP and universes. So the dichotomy of relevance to strictification isn't material/structural, but rather set-level / univalent. I think that's what I was trying to say, but didn't express very well.
Mike Shulman (May 03 2021 at 00:07):One could also go the other way and enhance HoTT to 2LTT, in which case one might be able to strictify with respect to the exo-equality.
Leopold Schlicht (May 03 2021 at 11:28):So although the MO discussion I linked to above was about ETCS and BZC, the same thing (structural statements with a material proof also have a structural proof) holds if one replaces BZC by a material set theory T appropriate for talking about largeness and proving the strictification theorem for large 1-categories and ETCS by a type theory T' that admits similar constructions as T, but where "large types" don't come equipped with an equality predicate offhand, right?
So T should be able to prove "every large category is equivalent to a large category that is strict", which is a material statement that can't be translated into T', but it implies the statement "every large category D is equivalent to UC, for some strict large category C", where U is the construction from strict large categories to large categories forgetting the equality predicate on the objects of C. This is the non-evil version of the strictification theorem (as proposed by Oscar in the 2-categorical setting) which can be formulated in T', and if the answer to my question above is "yes", then this would mean that a structural proof of this structural strictification theorem inside T' can be extracted from the material proof inside T in which the evil strictification theorem is used as an intermediate step, right?
Similarly for the strictification theorem in the 2-categorical setting.
(For me, type theory is a sort of "structural" set theory.)
Mike Shulman (May 03 2021 at 14:39):Leopold Schlicht said:
So although the MO discussion I linked to above was about ETCS and BZC, the same thing (structural statements with a material proof also have a structural proof) holds if one replaces BZC by a material set theory T appropriate for talking about largeness and proving the strictification theorem for large 1-categories and ETCS by a type theory T' that admits similar constructions as T, but where "large types" don't come equipped with an equality predicate offhand, right?
No, I don't think so. The classifying category of T' wouldn't be a 1-category, for one thing. You could hope for a similar statement to hold with a higher category, but no one has proven such a thing that I know of. And in order for anything of the sort to be true, you would certainly have to add to T' some axiom like "sets cover", which requires at least some notion of identity type for all types even if it's univalent rather than strict.
Leopold Schlicht (May 03 2021 at 15:15):Interesting. So you wouldn't even expect T' to be able to prove the non-evil version of the strictification theorem (the forgetful functor from strict large categories to large categories is essentially surjective)?
I would like to understand what we need to add to T' so that this is possible. Above you already mention that it works if one adds UIP, and now you are mentioning "sets cover". I only have a rough understanding of the former, which I think means that any two proofs of an equality (i.e., terms of an identity type) have to be equal. Why do these additional assumptions enable us to prove the non-evil coherence theorem?
Is it possible to formulate (and prove) the non-evil coherence theorem only on the set-fragment of HoTT? My naive opinion is that only because one talks about largeness, it doesn't necessarily has to mean that one leaves the set-level. (But this is very naive, I'm not really qualified to even use these words.)
Leopold Schlicht (May 03 2021 at 17:28):By the way I always wondered why the HoTT book defines a category to have a type of objects (but a set of morphisms). Why isn't it better to have a set of objects? I usually think about objects in a category not as being points in some space. :-)
Does this change of definition yield all the strictification theorems?
James Wood (May 03 2021 at 18:09):A concrete reason would be that the (large) type of sets is not itself a set, but rather a groupoid. More abstractly, you can see a set as a type whose notion of equality is well behaved, and because we don't talk about equality of objects, we don't need that equality to be well behaved (in contrast to the equality of parallel morphisms). Moreover, when you get the notion of univalent category (a category in which isomorphism is equivalent to equality (of objects)), it is then natural for the objects to form a groupoid, because there are often many isomorphisms between a pair of objects.
Mike Shulman (May 03 2021 at 19:46):Right: the objects of a category are points in a space, namely the homotopy 1-type (= groupoid) underlying the category. If you assume the univalence axiom, then the type of sets is not itself a set; so if you want to have a "category of sets" (which seems a reasonable expectation) you can't demand that the objects of a category form a set.
Mike Shulman (May 03 2021 at 19:49):James Wood said:
you can see a set as a type whose notion of equality is well behaved
Well, "well-behaved" is a value judgment. I think the notion of equality in the type of sets, assuming the univalence axiom, is quite well-behaved. It's just that it's not a mere proposition. (-: But it's much better-behaved than the notion of equality in the type of sets if you assume UIP, because in the latter case you can't say anything about when two sets are equal; whereas univalence tells you exactly when two sets are equal, and the answer is the same one that we use all the time in structural mathematics.
I'm sorry about nitpicking your words, but I don't want people to have the impression that types that aren't sets are "bad" or "pathological" in any way. They're actually much more natural than the behavior of large types under UIP.
Mike Shulman (May 03 2021 at 19:53):Leopold Schlicht said:
Interesting. So you wouldn't even expect T' to be able to prove that... the forgetful functor from strict large categories to large categories is essentially surjective?
Correct. Because T' should have models in which that statement is false, such as those mentioned on the "sets cover" nlab page. (And we care about these models, so "sets cover" is not really a good axiom to add.)
I would like to understand what we need to add to T' so that this is possible. Above you already mention that it works if one adds UIP, and now you are mentioning "sets cover". ... Why do these additional assumptions enable us to prove [the above statement]?
Under UIP, every category is already strict, so there is nothing to prove.
Under sets cover, what you get is a weaker statement, that every category is weakly equivalent to a strict one. Just take a set cover of the type of objects, and pull back the morphisms; the resulting functor is fully faithful (by definition of the morphisms) and essentially surjective (because you started with a cover), and its domain is strict by construction. (But it won't, in general, have an inverse functor going in the other direction, so it won't be a strong equivalence.)
Is it possible to formulate (and prove) the non-evil coherence theorem only on the set-fragment of HoTT?
Well, yes, you can prove that every category in the set-fragment is (equivalent to) a strict one, since by definition "a category in the set-fragment" means a strict category. But this isn't very useful, because for instance "the category of sets" doesn't live in the set-fragment.
Leopold Schlicht (May 04 2021 at 18:27):Ah, thanks, I see: I agree that one wants to have a notion of "large collection" so that "large collections" don't come equipped with a form of "equality proposition" on it (the collection of sets should be such a "large collection" and we generally don't want to talk about equality of sets). And the collection of all objects of a category should be such a "large collection". Although in my personal informal type theory I'm using in practice, I still don't think of "large collections" as spaces whose identity types aren't mere propositions, but as something like "sets" that just don't have any equality predicate (not even identity types failing to be mere propositions).
This was also what I had in mind when sketching, in an extremely vague form, the theory T'.
It seems to me that one of the conclusions we had in the conversation so far is that T' can't prove the (non-evil) strictification theorem. I think that's quite remarkable.
My current question then is: Can T' prove the coherence theorem (every formal diagram in a bicategory made up of associators and unitors commutes)?
Usually, this follows from the strictification theorem (for bicategories). If the coherence theorem isn't provable in T', perhaps this would be a serious philosophical argument for not believing in it. At least if one denies the meaningfulness of equality of objects, just as some people might deny the existence of infinite sets. Remarkably, the latter opinion denies the truth of an axiom (the axiom of infinity), while the former denies only a concept (the concept of equality between objects).
Mike Shulman (May 04 2021 at 18:42):Yes, T' can prove the coherence theorem. I think it's better to regard the strictification theorem as following (in classical mathematics) from the coherence theorem than the other way around. In particular, I don't know how to prove the strictification theorem without already having something essentially equivalent to the coherence theorem, although it's true that if you assume the strictification theorem you can derive the coherence theorem from it.
Morgan Rogers (he/him) (May 04 2021 at 18:42):Leopold Schlicht said:
Remarkably, the latter opinion denies the truth of an axiom (the axiom of infinity), while the former denies only a concept (the concept of equality between objects).
I'm pretty sure that the existence of an equality predicate is implemented as an axiom, it's just that it's more often taken for granted than the axiom of infinity.
Mike Shulman (May 04 2021 at 18:44):Morgan Rogers (he/him) said:
Leopold Schlicht said:
Remarkably, the latter opinion denies the truth of an axiom (the axiom of infinity), while the former denies only a concept (the concept of equality between objects).
I'm pretty sure that the existence of an equality predicate is implemented as an axiom, it's just that it's more often taken for granted than the axiom of infinity.
It depends on what you mean by "axiom" and "equality predicate". In type theory, identity types are usually specified by rules, with computational behavior, whereas an "axiom" in type theory usually means a bare element of some type without any computational behavior. However, if you consider only identity types "up to equivalence" then their existence can be asserted internally as an axiom.
Mike Shulman (May 04 2021 at 18:45):In first-order logic, I don't think the existence of equality can be formulated as an axiom, but has to be given by rules for forming atomic equality propositions. But in higher-order logic, you should be able to formulate it as an axiom -- although, as for up-to-equivalence identity types in type theory, an ordinary such axiom would only assert it for some particular type or family of types, rather than uniformly for all types.
Morgan Rogers (he/him) (May 04 2021 at 18:54):I can see why there is a need to make a distinction between "a rule of how first order logic works" and "an axiom in a first order theory", so apologies for the imprecision. Perhaps "meta-axiom" would be more appropriate. The point I was trying to make is that they're both rules formalising the assumptions we make about our logics/theories, and even if they are in some sense a level apart in some formulations, the distinction between them doesn't quite reach the heights of "remarkable" (for me, anyway :sweat_smile: ).
Mike Shulman (May 04 2021 at 20:01):Yes, I agree.
Leopold Schlicht (May 05 2021 at 12:46):Thanks (also to Morgan for starting the discussion about "axiom").
What's the idea of the proof of the coherence theorem in T'? I have to admit I only know the ideas explained in Leinster's Basic Bicategories, in which he sketches how the strictification theorem implies the coherence theorem. I don't yet see how this approach is based on "already having something essentially equivalent to the coherence theorem".
Is there any important piece of mathematics that isn't provable in T'?
Mike Shulman (May 05 2021 at 14:28):Oh, that's right. I always forget that in the special case of bicategories you can also prove the strictification theorem with the Yoneda embedding. It feels like cheating. (-:
Mike Shulman (May 05 2021 at 14:29):For the kind of syntactic proof of the coherence theorem that should work in , have a look at VII.2 of Categories for the working mathematician.
Mike Shulman (May 05 2021 at 14:30):Is there any important piece of mathematics that isn't provable in ?
Well, it's hard to say for sure since you haven't formulated precisely. But I would guess that much of mathematics can be done in it.
Leopold Schlicht (May 05 2021 at 16:20):Thanks!
Right, then let me put the question this way: Can each application of dubious strictification theorems you are aware of be replaced by an argument not involving talking about equality between objects? :-)
Leopold Schlicht (May 07 2021 at 19:55):Nobody an opinion? :P
My hope would be that the answer is "yes". It would be weird if it's really necessary to talk about equality between objects.
Oscar Cunningham (May 07 2021 at 19:57):I've never heard anybody arguing that there's some category-theoretic result that would be impossible to formalise in HoTT, so it seems that they can all be formalised without equality between objects.
Mike Shulman (May 07 2021 at 21:06):If we're talking about arguments involving finite-dimensional categories only, then I would expect that to be true, but there are cases where the replacement argument would be significantly different and longer, and I don't think it's actually been written down. For instance, there are a lot of powerful tools for working with strict 2-monads, which I would expect can also be done using pseudomonads (which a HoTT version would have to do), but it would be a lot more work.
Mike Shulman (May 07 2021 at 21:08):It's not always just a question of inserting lots of isomorphisms, either. For instance, many of the 2-monad arguments involve transfinite constructions, which are not always formulated in a way that generalizes directly to work with higher categories. Sometimes, for instance, a result may rely on proving that some function is a bijection by showing that it's injective and surjective; there's an analogous result for higher types, but you have to use a stronger notion of injection, and it might happen that the original proof of injectivity doesn't prove the stronger version. (You also have to know when to replace, say, coequalizers with codescent objects, etc.)
Mike Shulman (May 07 2021 at 21:10):On the other hand, if we're talking about infinite dimensional categories, then no one even knows how to define those in Book HoTT, and some people conjecture that it's impossible. The problem is that to define and work with those you need to be able to work with infinite towers of coherence, but it seems impossible to say what that means without either a strict equality to make it well-typed or an already-existing theory of -categories.
Mike Shulman (May 07 2021 at 21:11):A related problem is proving, inside HoTT, that the types form a model of HoTT.
Mike Shulman (May 07 2021 at 21:12):There's an active research area of writing down enhanced homotopy type theories that allow you to work with -categorical structures, e.g. two-level type theory and simplicial type theory and polynomial monad type theory.
Leopold Schlicht (May 08 2021 at 18:11):@Oscar Cunningham Thanks!
@Mike Shulman Interesting.
So one cannot do -category theory in HoTT?
Is there something like HoTT in which -categories instead of -groupoids are taken as the primitive concept, a synthetic approach to higher category theory?
I don't know why exactly, but the discussion made me wonder: Could there be hope in stating or proving a metamathematical statement along the lines of "every theorem in category theory has a constructive proof?" (Of course it's not literally true, but maybe with modifications like replacing functors by Makkai's notion of an anafunctor.)
John Baez (May 08 2021 at 18:22):Leopold Schlicht said:
Is there something like HoTT in which -categories instead of -groupoids are taken as the primitive concept, a synthetic approach to higher category theory?
Not yet, but I believe there will be someday. One reason Voevodsky used -groupoids as the primitive concept was precisely to avoid taking -categories as the primitive concept: he's written about this, and why he decided to avoid it.
Fawzi Hreiki (May 08 2021 at 18:26):I've seen some papers here and there on directed homotopy type theory
Fawzi Hreiki (May 08 2021 at 18:26):There's also a book by Marco Grandis on directed algebraic topology but I haven't had a chance to look at that
Mike Shulman (May 08 2021 at 22:44):Yes, this is what Emily Riehl and I were trying to achieve with our type theory for synthetic infinity-categories (which I mentioned before as "simplicial type theory"). Other people have continued to push this forward since, such as Buchholtz and Weinberger.
Mike Shulman (May 08 2021 at 22:47):Leopold Schlicht said:
Could there be hope in stating or proving a metamathematical statement along the lines of "every theorem in category theory has a constructive proof?"
No, I don't think so. Even leaving aside anafunctorial issues, and also obvious category-theoretic translations of logical statements like "Set is a Boolean category", there are plenty of category-theoretic results that use classical reasoning, like Freyd's theorem that a complete small category is a preorder, or the fact that every simplicial set is cofibrant, or that every accessible endofunctor generates a free monad.
Morgan Rogers (he/him) (May 09 2021 at 09:22):Mike Shulman said:
...there are plenty of category-theoretic results that use classical reasoning, like Freyd's theorem that a complete small category is a preorder...
There's a counterexample to that being true constructively in Part B of the Elephant, I believe, just as an example. It's always fun to ask "how true is this constructively", I fully support that kind of inquiry.
Leopold Schlicht (May 09 2021 at 15:20):I see, thanks!
Mike Shulman (May 09 2021 at 16:39):Morgan Rogers (he/him) said:
There's a counterexample to that being true constructively in Part B of the Elephant, I believe
Hmm, that seems unlikely to me, because it's true in all Grothendieck toposes. The only counterexamples I know of come from realizability toposes, which don't appear in parts 1 or 2 of the Elephant.
Morgan Rogers (he/him) (May 09 2021 at 18:55):I spent half an hour searching (my pdf version of the Elephant is frustratingly not searchable), and you were right, but I hadn't entirely misremembered. After B2.3.7, Johnstone says
There is a well-known result of P. Freyd which says that a complete small category must be a preorder. The proof of this result requires the law of excluded middle, and so one might expect it to fail for indexed categories over a non-Boolean topos ; we shall see that it does indeed fail in certain cases, in Chapter F2. However, in the main we shall be interested in applying 2.3.7 to internal posets...
So the counterexample is only alluded to there, and presumably shall involve realizability toposes, if it ever gets published :joy:
David Michael Roberts (May 10 2021 at 06:45):The example should already exist, somewhere. I doubt it's just on PTJ's shelf waiting for Part F to get written.
Morgan Rogers (he/him) (May 10 2021 at 07:07):Indeed, the nLab page contains references to Hyland's papers.
Mike Shulman (May 10 2021 at 14:25):Yes, of course. Although if I recall correctly there are some subtle points to do with the meaning of "completeness" for an internal category that may not be completely resolved.
Leopold Schlicht (Aug 11 2021 at 13:41):Mike Shulman said:
On the other hand, if we're talking about infinite dimensional categories, then no one even knows how to define those in Book HoTT, and some people conjecture that it's impossible.
I don't understand this. Can't one just use the definition of a quasicategory (as a simplicial set satisfying weak Kan extension -- which should be possible to formalize within HoTT)? After all, HoTT is a foundation of mathematics, so one should be able to formulate all usual definitions within it. Or what do you mean by "define"?
Mike Shulman (Aug 11 2021 at 16:58):Yes, one can define a quasicategory inside HoTT (or any other classical notion of higher category) as a structure built out of sets (0-types), as an instance of the fact that you can formulate all ordinary set-based mathematics in HoTT. The problem is that most naturally arising examples are not built out of sets, and this happens already for 1-categories: the type of objects of the category of sets is the type of sets, which is not a set (by univalence). So to have a useful theory of -categories in HoTT, we can't just import the standard set-based definitions, but we essentially have to do something new, defining a notion of -category built out of higher types.
Leopold Schlicht (Aug 12 2021 at 09:02):That makes sense, thanks!