38
$\begingroup$

One of the major motivations of Homotopy Type Theory is that it naturally builds in higher coherences from the beginning. One important setting where higher coherence requirements get annoying is higher category theory. It's easy to talk about $\infty$-groupoids in HoTT, they're just types and you build them as higher inductive types. What about the next step? How do you talk about $(\infty,1)$-categories? I looked around at the nlab and the relevant blogs, but didn't find anything.

The natural setup is that you have a type of objects and a (dependent) type of morphisms. But composition seems to run into all the usual difficulties of coherence in higher category theory. Does the HoTT point of view simplify things at all here?

Feel free to assume that I'm familiar with the discussion of ordinary categories in the HoTT book and the background in the HoTT book. On the other hand, also assume that I find all definitions of higher categories beyond dimension 2 at least somewhat confusing. My motivation is that I'm trying to understand what you would need to do in order to give a formal proof of the cobordism hypothesis in dimension 1.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Is this question about directed type theory? $\endgroup$
    – Andrej Bauer
    Commented Oct 24, 2013 at 20:31
  • 5
    $\begingroup$ Coherence (for simplicial types) seems to be precisely the stumbling block at the moment, cf Peter Lumsdaine's comment here. $\endgroup$
    – Zhen Lin
    Commented Oct 24, 2013 at 20:48
  • $\begingroup$ @AndrejBauer: I don't think so. I just want to talk about infinity categories inside ordinary non-directed HoTT. $\endgroup$
    – Noah Snyder
    Commented Oct 24, 2013 at 23:08
  • $\begingroup$ @ZhenLin: Do I understand right that you're saying that this is an open problem? $\endgroup$
    – Noah Snyder
    Commented Oct 24, 2013 at 23:16
  • $\begingroup$ I think this is an open problem, but I'm not enough of an expert to be sure $\endgroup$
    – David White
    Commented Oct 25, 2013 at 1:35

3 Answers 3

Reset to default
34
$\begingroup$

This is an important open problem. There are several imaginable approaches, including but not limited to:

  1. Mimic some commonly used homotopical definition of $(\infty,1)$-category inside HoTT. The most likely candidate seems to be complete Segal spaces, since they have a space of objects rather than a set of objects. This would require a definition of "simplicial type" in HoTT, which is another important open problem (which is motivating some people to try modifying type theory).

  2. Use a definition in a more type-theoretic style. The $\infty$-groupoids of HoTT are naturally "algebraic" a la Grothendieck/Batanin, so maybe it would be more natural to use a similarly algebraic definition of $(\infty,1)$-category. One could, for instance, try to encode an operad of a suitable sort with an inductive definition.

  3. Invent a sort of "directed type theory" whose basic objects are $(\infty,1)$-categories, in the same way that the basic objects of HoTT are $\infty$-groupoids.

  4. Leverage the fact that HoTT admits models not just in $\infty$-groupoids but in other $(\infty,1)$-toposes, noting that complete segal spaces live inside the $(\infty,1)$-topos of simplicial spaces. I proposed this here; Andre Joyal independently had the same idea.

At this point I wouldn't presume to bet on which approach will prove the best, or whether it will be something entirely different.

Improve this answer
$\endgroup$
9
  • $\begingroup$ Is it clear for any of these approaches that they will get around the stumbling block mentioned by Zhen Lin above? At the Barcelona conference this stumbling block was mentioned (in the context of whether a pullback diagram had to commute strictly or not) and someone referenced a comment of yours about Tarski Universes as a potential fix. The comment appeared here: groups.google.com/forum/#!msg/univalent-foundations/Glo7NgNvhJA/… $\endgroup$
    – David White
    Commented Oct 25, 2013 at 12:50
  • 3
    $\begingroup$ The stumbling block is exactly the difficulty involved in succeeding with approach (1), and probably approach (2) would require solving a similar problem. The issue with Tarski universes is unrelated and has to do with the interpretation of univalence in models built from set theory, such as simplicial sets. Joyal's "typos" are just a name for the input to these sorts of models, which other people call "type-theoretic fibration categories" or "comprehension categories" or lots of other things. $\endgroup$
    – Mike Shulman
    Commented Oct 26, 2013 at 14:56
  • 2
    $\begingroup$ As Noah mentioned below, Emily Riehl and I have now worked out some details of idea (4), and it seems to work fairly well. There's also now a concrete proposal for one possible modification of type theory that enables (1) to work, namely "two-level type theory" arxiv.org/abs/1705.03307 . $\endgroup$
    – Mike Shulman
    Commented Jun 25, 2018 at 18:54
  • 2
    $\begingroup$ Work specifically on approach (1) is arxiv.org/abs/1707.03693 $\endgroup$
    – Mike Shulman
    Commented Jul 5, 2018 at 4:10
  • 1
    $\begingroup$ @CAT If you're talking about the "simplicial type theory" approach (4), there is no general recipe. Some particular categories can be constructed, particularly if you can introduce universes with appropriate univalence properties. For instance, the category of groups should be definable from the category of sets, and similarly for other "algebraic" categories. But in general, in this approach one can't "put together a Segal type out of pieces" but rather has to construct it "synthetically" qua category (or simplicial space). $\endgroup$
    – Mike Shulman
    Commented Feb 13 at 23:42
10
$\begingroup$

Emily Riehl and Mike Shulman now have a preprint which builds a version of type theory which includes $(\infty,1)$-categories as certain kinds of types.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Indeed, was meaning to update my answer, thanks for sharing! $\endgroup$
    – Edouard
    Commented Dec 16, 2017 at 20:45
  • 3
    $\begingroup$ Right, this is a working out of the idea (4) among those in my original answer. $\endgroup$
    – Mike Shulman
    Commented Jun 25, 2018 at 18:53
8
$\begingroup$

While this question has an accepted answer, let me just mention that there is now a preprint by James Cranch about doing categories structured over homotopy types, you might be interested to have a look.

Improve this answer
$\endgroup$

You must log in to answer this question.

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