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.
That's a simple one, but: what is the notion of equality in infinity-categories? Do we need to have any? I thought the goal of having infinity-categories was precisely to get rid of (non proof-relevent) equalities, but I guess there is still a notion of equality since in the Riehl-Verity paper, they speak of equality of morphisms and of invertible cells. In that case, what do we endow with a notion of equality, is it just morphisms for $k>1$?
I don't think the goal of infinity-categories is to get rid of equalities. It is more about allowing a spectrum of weaker equalities in your toolbox. I am pretty sure that, in any model for infinity-categories, you would define the majority of your homotopy-based comparisons with equalities.
For instance, defining an isomorphism would require equalities when writing the axioms:
Now, there are theories for infinity-categories that may rely on spheres and discs, so that equalities would be abstracted away, but even for these, you would usually have retractions that would model equalities.
Edit: Also add to this that you have to define the sources and targets of your homotopies, which are based on equalities that relate discs of different dimensions
the situation is quite similar to that of 1-categories: there are some statements that are evil but can appear with specific choices of presentations of the theories. In 1-category theory, you can talk about equality of objects, but it's evil. This is the same with ∞-categories: in most presentations of the concept, like with quasi-categories, you can talk about equality of morphisms, but it's stricter than what you probably want (and it's also evil).
you could say it's part of the presentation but not of the language of ∞-categories
Okay thanks!
Josselin Poiret said:
the situation is quite similar to that of 1-categories: there are some statements that are evil but can appear with specific choices of presentations of the theories. In 1-category theory, you can talk about equality of objects, but it's evil. This is the same with ∞-categories: in most presentations of the concept, like with quasi-categories, you can talk about equality of morphisms, but it's stricter than what you probably want (and it's also evil).
In the case of categories, equality of morphisms is part of the definition, while equality of objects is not necesssarily given, but here I guess that in the actual definition we still require to have a definition of equality (or an equivalence relation) on morphisms, even if we don't use it?
Everything said above really only applies if we work in a set theory as our foundations of mathematics, where everything comes with a propositional-valued equality, including -categories and their hom-sets.
In dependent type theory, equality in -categories (i.e. Rezk types in dependent type theory) and their hom-types is given by the identity type, but identity types are not required to be (-1)-truncated (i.e. proposition-valued) and instead they can be untruncated (i.e. valued in -groupoids). So people working in an ambient dependent type theory don't really run into problem of evil with -categories that people working in set theory do.
They do, however, run into problems defining untruncated -categories.
Jonathan Arnoult said:
In the case of categories, equality of morphisms is part of the definition, while equality of objects is not necesssarily given, but here I guess that in the actual definition we still require to have a definition of equality (or an equivalence relation) on morphisms, even if we don't use it?
If you suppose that you have a given equivalence relation on morphisms that is not just the ambient equality, you are working with E-categories and not the usual 1-categories. This is actually something that comes up a lot when formalizing category theory in proof assistants, especially when one doesn't want to postulate extensionality properties like funext
in any case, your ambient language lets you still ask whether two morphisms are equal propositionally, without any regard to your chosen equality relation. The same can be said for objects
Mike Shulman said:
They do, however, run into problems defining untruncated -categories.
Not really. Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz in section 2.1 of their paper Directed univalence in simplicial homotopy type theory defined hom-types, Segal types, and Rezk types in terms of an arbitrary distributive lattice in ordinary dependent type theory. What becomes hard to do is proving various properties of untruncated -categories since you have to transport identifications in everywhere.
I didn't say the problems have no solutions! Just that they exist.
And for the record, I wouldn't regard those as "definitions of -categories" in the ordinary way that people use the word "definition", as they are primarily synthetic rather than analytic.
Madeleine Birchfield said:
Mike Shulman said:
They do, however, run into problems defining untruncated -categories.
Not really. Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz in section 2.1 of their paper Directed univalence in simplicial homotopy type theory defined hom-types, Segal types, and Rezk types in terms of an arbitrary distributive lattice in ordinary dependent type theory.
Just as a remark, this portion of the paper is summarizing the work by Emily Riehl and Mike Shulman in their paper on the matter. There they also included as an additional sort of judgmental structure precisely to avoid needing quite so many transports. In our setting (with modalities and what not), including this judgmental structure was more headache than it was worth.
There are "definitions" of untruncated -category that can be given in type theories, but not, so far as is known, in "ordinary" dependent type theory. It's possible in two-level type theory, for instance, and ought to be possible in displayed type theory.