The precise technical innovations of HoTT are just that, technical. I&#x27;ll try to focus on a practical consequence of those innovations.<p>If you know anything about data structures you know that a lot of times, 2 different instances of the structure will be considered &quot;equal&quot; even though they aren&#x27;t exactly the same.<p>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:<p><pre><code>    tree = node(tree, tree) | leaf(int)
</code></pre>
but you will consider things to be the same even if they aren&#x27;t exactly the same tree, since you are externally presenting a list:<p><pre><code>    node(node(leaf(1),leaf(2)), leaf(3))</code></pre>
and
    node(leaf(1), node(leaf(2), leaf(3))
for example.<p>However when you implement all of your list operations (which will include tricky rebalancing), you will have to manually check it, which is hard.<p>In HoTT you can choose to have the type system help you check it by saying<p><pre><code>    tree = node(tree, tree) | leaf(int)
</code></pre>
and asserting to the type system things like<p><pre><code>    node(node(t1,leaf(n)), t2) = node(t1, node(leaf(n), t2)
</code></pre>
then when you write your rebalancing function the type system will have you prove that you preserved equalities like this.<p>You can already simulate this in theorem-proving languages but the technical details of HoTT allow you to<p><pre><code>    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.
</code></pre>
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.<p>All in all, if you&#x27;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 &quot;next generation&quot; of proof assistants.