They seem to be necessary if you want a notion of "equivalence" (for both values and types) that enables you to make functions, operations, constructs etc. independent of any notion of "underlying representation" as well as seamlessly applicable across equivalent 'representations'. This is desirable in both higher mathematics (where homotopy types were first developed) and software engineering, for much the same reasons.
Isn't this what a homotopy category is for though?
Could you explain this to a layman with an interest in FP?
I read about this a while ago, I'm not an expert but this is my take on it:
In homotopy type theory an equivalence of types is a first class value that you can manipulate. And also you can separate types from their 'implementations'. Classic example is you have a Nat type, with a Peano construction (Nat is a zero or a successor of a Nat.) This is not very efficient, but you write functions with it, prove things etc. It's time to optimize, and you change your Nat implementation to something more efficient (e.g. a Nat is Zero, or twice a Nat, or twice a Nat + 1). Your functions and proofs that you wrote with the previous implementation still will work and your type signatures won't have to change