# How do you define (infinity,1) categories in Homotopy Type Theory?

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.

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

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.

• 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/… – David White Oct 25 '13 at 12:50
• Actually, now that I think about it, I remember a talk by Andre Joyal about Typos which seemed like it might avoid this issue. As I recall, he was suggesting this as an alternative approach to univalent foundations, so it might lose the feature of being programmable. Are you familiar with Joyal's Typos? Do you think they get around the strictness issue? Please also correct me if I've misunderstood the problem or the basic points of Joyal's approach. – David White Oct 25 '13 at 12:59
• 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. – Mike Shulman Oct 26 '13 at 14:56
• 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 . – Mike Shulman Jun 25 '18 at 18:54
• Work specifically on approach (1) is arxiv.org/abs/1707.03693 – Mike Shulman Jul 5 '18 at 4:10

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.

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.

• Indeed, was meaning to update my answer, thanks for sharing! – Edouard Dec 16 '17 at 20:45
• Right, this is a working out of the idea (4) among those in my original answer. – Mike Shulman Jun 25 '18 at 18:53