[digama]

I don't believe you could vary Mizar to the extent that it mimics HoTT. Much of the basic properties that follow from the axioms Mizar uses (roughly ZFC + the Tarski-Grothendieck axiom) are built in to the internals of the Mizar prover, in order to increase its proving capability, at the expense of tying it to its axiom set.

By contrast I can tell you that Metamath (http://us.metamath.org/mpegif/mmset.html), whose main library is also built on ZFC, does not at the most basic level assume any axioms at all (not even first order logic), so it is possible to do type theory or HoTT with no change to the verifier.