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