I agree -- most fields of math are happy to establish their own axioms, and leave the reducibility of those axioms to some "foundations" as an exercise -- an important one, but not one that necessarily furthers the field itself.
However, Voevodsky's stated aim for his Univalent Foundations project was not to formalize everything under a grand theory of everything. He got the bejeebus scared out of him when one of his results was very, very subtly wrong, in a way that was difficult for mathematicians to verify for years, even given a reasonable inkling of a counterexample. So he sought to improve the state of the art in proof verification.
You might argue, it's better to produce a verification tool for one field of mathematics than all of them at once. But you'll have a hard time finding any significantly complex theorem that doesn't draw insight from multiple places. (Arguably, that's why they're significantly complex in the first place). And all fields of mathematics have some basic elements in common. So, I'd argue, you're unlikely to do a good job for any but the most narrow domains of mathematics without seeking some level of generality.
Any "foundation of mathematics" can be used for this purpose, and plenty of theorem provers have been built on each (Twelf, PVS, Agda). The draw of category theory is that it seems to capture at a fundamental level many of the basic conceptual elements we see across mathematics. (Homomorphisms are so universal it's not even funny.) It seems reasonable to pick something that starts us closer to where we want to be; the difficulties we encounter are more likely to be fundamental problems and not issues of encoding.