Before I attempt to address your specific questions, let me give a thought provoking non-answer:

Reverse mathematics is impossible (and irrelevant) in HoTT!

This is because HoTT fully supports *proof-relevant mathematics*, so when you refer to a theorem you necessarily refer to a proof of that theorem. The question whether the hypotheses are necessary doesn't make sense in this context since the hypotheses are part of the theorem itself!

Now that your thoughts have been provoked, let me amend the above statement:

HoTT is not the end of reverse mathematics!

Actually, it just makes the reverse (and constructive) mathematics questions even more obvious. The most fundamental reason why reverse mathematics exists is the incredible power of the existential quantifier. In HoTT, that is immediately obvious. A plain existential statement is interpreted as a dependent sum type in HoTT: "$\sum_{x:A} P(x)$ is inhabited" is the right way to say that "there is an $x$ of type $A$ such that $P(x)$." By definition, every inhabitant $x:A$ of this type is equipped with a justification of $P(x)$. To get the usual existential quantifier, one must truncate $\sum_{x:A} P(x)$ to a proposition. This raises the question: can this truncation be reversed? What are the necessary hypotheses to reverse this truncation? This is what reverse mathematics questions get turned into when translated into the language of HoTT. Note how "mathematical" the reverse mathematics question has become! This is no surprise to practicing reverse mathematicians but it is very interesting how reverse mathematics becomes less mythical in this context.

I will now add what I know about each of your questions. Since I'm still learning about HoTT, these answers are far from complete or definitive. I hope that experts will chime in at some point.

The above sort of addresses this question. An additional difficulty is that it seems that there is still some work to be done in understanding models of HoTT. The soundness and completeness theorems obtained by Awodey & Warren and Gambino & Garner are almost there but Awodey points out some subtle issues. I don't know if these issues are problematic enough to make it difficult to establish non-provability results for HoTT.

HoTT is perhaps too strong for use as a base system for classical reverse mathematics. The reason is basically the same as why ZF is often too strong for that purpose. Note, however that even ZF is not completely useless. For example, as witnessed by a great deal of literature, ZF is a perfectly fine base theory for the analysis of choice principles. HoTT is more promising as a base system for constructive reverse mathematics but the constructivity of the univalence axiom is currently an open problem.

I don't think the univalence axiom is that problematic. The law of excluded middle always clashes with the propositions-as-types interpretation. The correct way to formulate the law of excluded middle in HoTT is to restrict it to propositions — types with at most one element. This version of the law of excluded middle does not clash with univalence and captures all of the normal uses.

I don't think anyone has addressed the question whether HoTT is a conservative extension of BISH (say) or how far it is from being a conservative extension.

It's difficult to make a comparison. The base system RCA_{0} was explicitly designed to capture basic computability theory. HoTT wasn't designed that way but other aspects of computability were important design components.

I don't see much gain in using proof assistants for reverse mathematics but I might be nearsighted.

Yes, some additional axioms such as propositional resizing, the law of excluded middle, and the axiom of choice have been analyzed to some extent. HoTT is so young that very little of this has been done yet.