Comment by orangea

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?

My perspective has always been that it can't.