What are the applications of homotopy type theory to everyday programming?


What are the applications of homotopy type theory to everyday programming?

I know of only two applications, neither of which I understand:

  • "Homotopical Patch Theory"
  • "HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics"

Is there a capsule summary of how HoTT is relevant to these problems?

Is there a general kind of programming problem for which HoTT is suited? Based on the applications so far, is it likely that future applications will all have to do with program efficiency? Or might there be applications to distributed systems, for example?

Higher inductive types strike me as the most obviously "new" thing from a programmer’s point of view. Is there a capsule summary of why programmers might use higher inductive types? Do these applications only have to do with program correctness, or do they also give us the ability to solve problems differently?

I know it’s early days and that we probably don’t know what the applications may be, but it’s also likely that more is known now than several years ago when the articles above were written.