I'm interested in the machine translation of mathematics from informal to formal (a la Ganesalingam in *The Language of Mathematics*). As a first step, I am designing a computer language for expressing mathematical definitions, theorems, and arguments that would at some later point be amenable to a small formalization kernel. (At this point, the language looks like a pared-down Isabelle/ZFC with support for functions not defined on full domains, realm-like objects, and a weak sense of parametric types and polymorphic functions).

This translation project, which is already sizable, would be the first step towards making a general mathematical knowledge management system/formalization system. The goal of this system would be to be sufficiently useful and easy to use that it sees adoption by those who don't intrinsically care for formalization. Cf. this old MO post for previous community thoughts about such a system.

Recently, the system of univalent foundations by Voevodsky has brought general interest back into formalization. The system of univalent foundations, like the type theoretic conceit that "a proof is an instance of a proposition type" that univalent foundations is ultimately based on, is illuminating and quite beautiful, and I found my brain exploding repeatedly while reading the IAS book on the subject (available here).

Questions:

Do univalent foundations provide a better structure for the introduction of definitions and the statement of theorems than the system I describe in the first paragraph? Can the intensional/extensional questions resolved by the univalence axiom in practice be handled by realms?

If univalent foundations provides this better foundation, will users who try to understand definitions and theorems in this system necessarily need to understand univalent foundations?

Which kinds of formal arguments are easier to make using univalent foundations, and are some kinds of sentence-by-sentence translations of informal proofs more feasible?

Is full-scale reflection in the sense of John Harrison's Metatheory and Reflection in Theorem Proving able to introduce the advantages of univalent foundations into a less well developed underlying type theory?

I am working on this problem because it seems important and not because I am particularly suited for it, so any thoughts would be very helpful.