How can homotopy type theory, as opposed to non-homotopy type theory, help us with "verification of systems/hardware and formalization of math" outside of homotopy theory itself?
From my experience ability to turn equivalences to equlities and vice versa is very usefull. Without this you are ending in setoid hell - intracable mess of isomorphism. I suspect that also Higher Inductive Types have lots of potential to simplify practical verification effords (apart from obvious usecases of quotients and truncations)