What are the implications of Homotopy Type Theory?
I won't lie: I don't understand the homotopy part of homotopy type theory. But I have a decent grasp of Univalence, which is the axiom at the heart of Homotopy Type Theory (HoTT).
The main idea of univalence is that we treat equivalences (essentially, isomorphisms) as equalities. When two types are isomorphic, you have a way to get from one to the other and back, and the round-trip is the identity in both directions. But there's no way to lift properties between isomorphic types: if you have a proof that 2 is the only even prime for unary natural numbers, you can't automatically lift the proof of that property to binary natural numbers, even though you can convert 2 back and forth between the formats.
The eliminator for equality (sometimes also called the $J$ axiom) allows you to lift any property between equal things. So if we have an equality for every isomorphism, then we could transport the above property from unary to binary numbers. This is what univalence gives us: an axiomatic way to lift properties over isomorphisms.
The main implications of this are:

For programming: univalence is specifically about equality types, which are dependent types, so it only really affects dependently typed languages. What it allows us to do in those languages is to write code using efficient data structures, show that those structures are isomorphic to simpler structures, prove things about the simpler structures, and automatically lift those proofs back to the automatic structures.
For math, it makes formal something that has been implicit for a long time, which is that mathematicians tend to treat isomorphic things as if they were equal. Univalence provides a foundation that justifies this. So it brings the &quot;formalized&quot; math of proof assistants closer to the way mathematicians think of math.

There are also some cool things you can do with univalence. You can define Higher Inductive Types (HITs), where in addition to giving data constructors for inductive types, you give path constructors, which are equalities that must hold. When you pattern match, you then have to show that you preserve these equalities.
HITs allow you to do things like &quot;define integers as a natural plus a sign but, but ensure that positive and negative 0 are truly equal.
However, there are some strange consequences to univalence. First, it means that we cannot have $Refl : x \equiv x$ as the sole way to construct an equality proof, because univalence lets us construct equalities between things that are definitely not syntactically identical. This means that univalence is incompatible with &quot;Uniqueness of identity proofs&quot; and axiom $K$. In practice, this means that the rules of dependent pattern matching must be weakened to be consistent with univalence. Jesper Cockx has a whole line of research on how to do this well.
The other problem is that we lose &quot;canonicity&quot; i.e. the idea that every term can be fully evaluated to a value in canonical form. For equality, Refl is the only canonical proof of equality. So this means that when running programs, sometimes we get &quot;stuck&quot; on the use of univalence as an axiom. This makes sense: we basically said &quot;pretend I have a function that transforms isomorphisms into equalities&quot;. We never gave that function, so if we try to evaluate code that calls it, we'll get stuck.
The main effort to solve this problem is Cubical Type Theory. Cubical models equality in such a way that canonicity is preserved, but univalence can be proved as a theorem in the language. So univalence is now not an axiom, it's an actual function that can be applied.
If you're interested in this more, there are two main resources I'm familiar with. The HoTT Book is the canonical reference. There's also  Univalent Foundations in Agda, which is less focused on the homotopy theory, and more on the implications that univalence has for logic. I'm sure there are also more books I'm not familiar with. The Cubical Agda paper is also good.