I don't think Voevodksky himself has any constructivist leanings. The univalent foundations developments make use of various axioms that have no known construct

I don't think Voevodksky himself has any constructivist leanings. The univalent foundations developments make use of various axioms that have no known constructive meaning (e.g. the law of the excluded middle, and the famous univalence axiom itself), and which are motivated because there are known models in which they hold. On the other hand, many of his collaborators are interested in the project precisely because it uses Coq and they like constructive mathematics. So the HoTT book only uses exluded middle when necessary (and carefully tracks where), and developing a computational interpretation of univalence is considered to be an important task. Edit to add: So why would someone who doesn't care about constructivism want to use Coq? Because it's based around typed objects. Apparently, homotopy theorists had for a long time been aware that instead of basing mathematics on sets, and then constructing equivalence classes on top of those, you could take homotopy types as primitive.. something like basing mathematics on blobs rather than points. This was all considered theoretical and impractical--until someone noticed that the logic provided by Intensional Type Theory (as implemented in e.g. Coq) can be considered to do exactly this!