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:
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).
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.
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.
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.
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.
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.