The precise technical innovations of HoTT are just that, technical. I'll try to focus on a practical consequence of those innovations. If you know anything abo

The precise technical innovations of HoTT are just that, technical. I'll try to focus on a practical consequence of those innovations. If you know anything about data structures you know that a lot of times, 2 different instances of the structure will be considered "equal" even though they aren't exactly the same. For an overly simplistic example, if you implement a list as a binary tree so that you can support things like append faster you might have a type like this: tree = node(tree, tree) | leaf(int) but you will consider things to be the same even if they aren't exactly the same tree, since you are externally presenting a list: node(node(leaf(1),leaf(2)), leaf(3)) and node(leaf(1), node(leaf(2), leaf(3)) for example. However when you implement all of your list operations (which will include tricky rebalancing), you will have to manually check it, which is hard. In HoTT you can choose to have the type system help you check it by saying tree = node(tree, tree) | leaf(int) and asserting to the type system things like node(node(t1,leaf(n)), t2) = node(t1, node(leaf(n), t2) then when you write your rebalancing function the type system will have you prove that you preserved equalities like this. You can already simulate this in theorem-proving languages but the technical details of HoTT allow you to 1) Directly encode these statements in the type system. 2) Get some properties of equality for free. 3) Lift functions on isomorphic data structures for free. The 3rd one basically means that if you prove your trees are equivalent to linked lists you can use any function that uses lists for your trees and vice-versa. All in all, if you're just interested in programming HoTT is probably not important to you. But if you work on verifying things like safety-critical systems or complicated mathematics using theorem proving assistants HoTT is probably going to be a big influence on the "next generation" of proof assistants.