I think the best way to understand why homotopy type theory related stuff is interesting from a computer science perspective is that is a more satisfying account of extensional equality than any prior version. Lots of attempts have been made previously to add extensionality features to type theory that have been missing relative to e.g. set theory, but they often have some kind of caveat to them that is kind of unsatisfying. One might say that HoTT solves these issues because the mathematics is appropriate for a proper computational interpretation of what equality is, and trying to follow orthodox mathematical practice was part of the problem with previous approaches.
So, what is the difference? Traditionally people think of equality as being like an intrinsic property. Two things are equal when they "are actually the same" or something. This shows up in approaches to equality wanting to make it computationally irrelevant. There's nothing interesting about a proof that two things are equal, because they just are equal, and the proof has nothing to record.
However, this is not how intensional Martin-löf type theory works, actually. Values of identity type are computationally relevant, and the eliminator only reduces when the value computes to
refl. So in some sense, it leaves open the possibility that we can have non-trivial proofs that say how two things are equal, not just that they are equal. It just happens that there are no basic ways in the usual presentation to say how two things are eqal other than 'they just are.' In some ways, induction already introduces at least open terms of identity type that do not behave exactly like the 'these two things just are equal' term (
refl). HoTT just wishes to add new closed terms (hence the difficulty with computational behavior).
In some ways, this notion of non-trivial ways of how two things are considered equal is no surprise computationally. In type theory we often consider two things 'actually the same' when they really aren't. $λx.x$ is the same as $λy.y$ when we are using the α rule, but they are clearly not exactly the same symbol strings. And we have different collections of rules we may use at any given time to determine which symbol strings we consider 'actually the same;' α vs. α-β vs. α-β-η. So it is clear that 'actually the same' is a fictional idea, not reality.
The thing that most easily allows us to pretend that these technically distinct things are actually the same is decidability. It's easy to test whether two lambda terms are α equivalent, so we don't really need to keep track of how they are α equivalent, since we can just test them whenever necessary. Of course, we also need to not be able to tell the difference between α equivalent things anywhere. But then we can just say that α equivalent things are equal via 'they just are.'
But, this doesn't work for extensional equality of things like functions or quotients. It may not be possible to automatically decide that two values of type
T are related by relation
R for the purpose of introducing equality in
T/R. In set theory, this is explained by saying that values of
T/R are 'equivalence classes' of
T, but this is not really a sensible explanation computationally, because it may not be possible to compute that equivalence class.
Older approaches to adding quotients to type theory generally involve allowing you to prove equality explicitly via
R, but then maintaining the fiction by throwing away the proof, and making sure no one can ever really ask for it. The HoTT approach is to not throw it away. There are actual values of the identity type that contain witnesses of
R. When we define functions from
T/R, we give values for inclusions from
|y|. And if
r : R x y, we also give a case that receives
r, explaining how
|y| are related, so that we can use it to explain how to mediate between their images.
This essentially eliminates careful engineering necessary to avoid undecidable problems for these sorts of constructs, because we aren't just discarding the provided evidence. These content-ful mediations also give richer ways for constructions to 'respect' the equalities of other things, which is useful. The type theories that make all this work have pretty complex engineering of their own, but in a way it seems satisfying to take seriously the idea of computing explanations for how things may be interchanged, rather than merely ensuring that no one will care if they are interchanged.
A last aspect, and the genuine "homotopy" one arguably, is that it makes sense to consider two things to be equal in actually distinct ways. In fact, it makes sense to consider an actual single thing equal to itself in distinct ways. This shows up readily in extensional equality of types. Traditional equality of types is very intensional; only types defined the same way are equal. But, as long as we have invertible mappings between two types, we could imagine translating things written for one to the other. This is what univalence allows, making types with invertible mappings between them equal.
But, for instance, there are two distinct invertible mappings from
Bool to itself: the identity function and
not. So, even though every construction respects these mappings, and we are able to consider them equalities mediating from
Bool to itself, they are themselves distinct. This suggests a couple things.
The essential feature of equality is preservation by all constructions, not that things are exactly the same in exactly one way.
It might be interesting to consider other proofs that things are equal to not necessarily be 'the same' proof as every other. For instance, perhaps the multiple ways of β reducing terms with multiple redexes might not be considered exactly the same proof. Of course, if we do want to consider them the same, HoTT also tells us that we can do so by having a non-trivial mediation between different reductions that explains how to reorder the individual reductions (say).
I think it's also reasonable to take the position that these should genuinely be called something different, like "path", while "equality" is reserved for situations where there are mediations 'all the way up', possibly becominge genuinely trivial above some level (although that isn't necessary). But this is a novel and potentially very useful notion of extensionality for types/the universe that was not (to my knowledge) being considered in type theory prior to HoTT.
Definitions that allow you to create types that work this way by fiat (like HITs, mentioned in the other answer) also seem potentially very interesting for programming. For instance, one could define the lambda terms with distinct proofs of β equivalence, although I'm unsure what exactly one would do with them.