So I am pretty sure I know how to combine what we know about HoTT with what we know about rewrite systems and constraint solvers in simpler logics, and use it to implement extremely powerful general-purpose proof automation in Coq without any axioms. BUT
Coq might not be the most flexible code base to do that on. How about doing it with Cur instead? Dependent types in an extensible programming language, perfect substrate on which to implement new kinds of proof automation.
Read my blog!