Mike Shulman has a good discussion of what exactly needs to be shown in his
- Michael Shulman, "The univalence axiom for inverse diagrams" (arXiv:1203.3253)
The issue is that in the type theory the classification of objects is by strict pullbacks. So roughly the problem is that one has to show the object classifier of a random $\infty$-topos is, when the latter is presented by a type-theoretic model category, presented by an object which classifies other objects by strict pullbacks with strict respect for composition. Establishing this in generality is (or would be) a kind of semi-strictification result for $\infty$-toposes.
See also the other references in the nLab entry.
That description of the three directions is not too bad, although they are not of course completely separate, nor does everything called HoTT fall under one of them. Also, I'm not sure whether this applies to you, but I always point out that it is potentially confusing to say "topology" when what is meant is "homotopy theory", i.e. "$\infty$-groupoid theory" — all "spaces" appear in HoTT only up to homotopy.
Some people would like to write a proof checking/generating client that is sufficiently expressive so that you can actually do mathematics in it.
I'm not sure what use a proof checking program would be if you couldn't do mathematics in it... (-:
But yes, I think your description of point 2 is roughly accurate. Point 1 is just about using the model in the other direction: if you prove something in the type theory, then it's true as a statement about spaces. In particular, if you calculate something like a homotopy group of a sphere in the type theory, then it's also a true statement about the homotopy groups of spheres in classical algebraic topology. And in fact we've done this in a few simple cases, like $\pi_n(S^n)$ and $\pi_3(S^2)$, so it better ought to be credible. These proofs are different from the classical ones, elegant in a certain sense, and relatively easily formalizable in a proof assistant. (Notice that I'm talking about different proofs of known results here; it's not inconceivable that the new methods of HoTT might lead to proofs of new results even in classical homotopy theory, but I expect that day is far in the future.)
As for point 3, type theory in general has a lot of advantages over set theory as a foundation for mathematics. Among other things, it requires less arbitrary "encoding" to represent math, it more closely matches mathematical practice, and it can be more easily programmed in a computer, producing small "proof term" certificates that can be easily verified. UF/HoTT potentially fixes some of the disadvantages of traditional type theory, such as a lack of well-behaved quotients and the problem of transporting structures across equivalences, so it's even better. And in addition to traditional mathematics, it also includes new mathematics such as the "synthetic homotopy theory" calculations of homotopy groups mentioned above.
Finally, a point that I always emphasize: HoTT has many models other than the "standard" one in spaces. Roughly we can use any "$(\infty,1)$-topos" (although there are coherence questions still work in progress). This means that when we prove something in UF/HoTT (such as a homotopy group calculation, or any part of traditional mathematics that we might formalize using it as a foundation) the result is more general than in classical homotopy theory, since it is true in any of the models.
Best Answer
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.