6
$\begingroup$

This is a soft-question. But please let me know if its not suitable. My question is essentially what the title asks but I want to elaborate on a few things.

I know Emily Riehl uses a type theory to formalize a synthetic theory of $(\infty , 1)$-categories. This type theory is essentially homotopy type theory augmented with a directed interval type. I've also seen entirely new new type theories proposed for the study of $(\infty,\infty)$-categories, such as opetopic type theory.

Why do we need to introduce so much machinery beyond homotopy type theory in order to study higher categories? I have studied a bit of HoTT. It is, in part, supposed to provide a synthetic theory of $\infty$-groupoids. I a have seen on nLab that the language of HoTT is thought to provide the internal language of an $(\infty,1)$-topos. Additionally, formulating regular $1$-category theory in HoTT feels very natural.

So what in particular makes the generalization from $\infty$-groupoids to higher categories so difficult? I understand that higher categories are essentially directed in a way that higher groupoids are not. But I'm wondering if anybody can point to a particular point of difficulty in developing higher category theory in HoTT. And how proposed solutions, such as Riehl's language and opetopic type theory, fix this.

$\endgroup$

1 Answer 1

8
$\begingroup$

The main thing that makes it difficult is what I call the "problem of infinite objects". Any explicit definition of an $\infty$-dimensional categorical structure that one can write down involves infinitely many sets or types, related by some dependencies and operations.

For instance, one classical model for $(\infty,1)$-categories is Rezk's complete Segal spaces (which were also the inspiration and semantics for the directed type theory that Emily and I introduced). A CSS is a diagram on the simplex category, consisting of one space for each natural number and simplicial operators between them. This is a natural notion to try to formulate in HoTT, where the types act like spaces. But in classical homotopy theory we have a notion of strict equality which we use to formulate the functoriality property of a simplicial diagram. In plain HoTT we don't have this, so if we go about it naively we would have to talk about a simplicial diagram that's functorial up to all higher coherent homotopies. But unfortunately, there's no obvious way to talk about "all higher coherent homotopies" unless we already have defined an internal notion of $(\infty,1)$-category!

This isn't a problem for 1-categories, where there is only a finite amount of coherence. Similarly, one can define 2-categories, and so on, in principle reaching $n$-categories for any finite $n$ (although it would be impractical for anything much larger than 2).

A natural way to try to get around this problem is to leverage type dependency, since that gives us an indirect way to access and control strict equality. For instance, if $f:\prod_{x:A} B(x)$, then its composite $A \xrightarrow{f} (\sum_{x:A} B(x)) \to A$ with the projection is strictly (i.e. definitionally) the identity. And it is possible to define certain infinite-dimensional dependency structures internal to HoTT, such as globular sets. But to date, no one has succeeded in defining in this way a sufficiently rich structure, such as simplicial or even semisimplicial sets, that could serve as the basis of an internal definition of $(\infty,1)$-categories.

Another solution is called "two-level type theory", which reintroduces a strict equality that's flexible enough to be used in roughly the same way as strict equality in classical homotopy theory.

The solution that Emily and I proposed gets around this in the same way that ordinary HoTT gets around the analogous problem for $\infty$-groupoids. In ordinary HoTT the types are the $\infty$-groupoids, so we don't have to define them internally. Similarly, in our simplicial type theory, the types are the $(\infty,1)$-categories, so we don't have to define them. (Actually it's more complicated than that: the types include the $(\infty,1)$-categories, but strictly, so we do have to make some definitions to cut the latter out of the former. But the main point is that we don't have to manually define all the higher structure; it's encapsulated in a single type, just the way a single type in ordinary HoTT encapsulates all the structure of an $\infty$-groupoid.)

$\endgroup$
3
  • $\begingroup$ Thank you so much, this was very helpful! $\endgroup$ Apr 15, 2022 at 19:50
  • $\begingroup$ Is that what A type theory for synthetic ∞-categories is about? $\endgroup$
    – SamB
    Aug 9, 2023 at 1:25
  • $\begingroup$ @SamB Yes, that's the paper in which Emily and I introduced the type theory referred to in the second paragraph of the original question, and which I referred to a couple of times in my answer. $\endgroup$ Aug 9, 2023 at 17:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .