Personally I don't think it has any practical applications, but rather that this continues the trend of using the military to fund fundamental research. The mai

Personally I don't think it has any practical applications, but rather that this continues the trend of using the military to fund fundamental research. The main interest would probably be that HoTT allows for automatic theorem proving of more interesting theorems compared to other axiomatisations. It was originally designed to be able to do higher homotopy theory synthetically. The Lean theorem prover has actually dropped HoTT support. There is a certain chance that interest will vane after the founder Voevodsky died.