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.