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.



How do you define (infinity,1) categories in Homotopy Type Theory?
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](http://golem.ph.utexas.edu/category/2012/06/directed_homotopy_type_theory.html); 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.


