Higher inductive type: what for?

Question

The typical example of higher inductive type (HIT) is the circle $S^1$ that is nicely described here. I understand HITs are convenient if you want to do homotopy theory within type theory. But what does it bring the computer scientist? Are there interesting data structures that could not be defined without an HIT?

Answer 1

Good question. To start with I should be clear that I think HITs are probably much more interesting to a homotopy theorist than to a computer scientist. However, it seems that they are not completely devoid of interest to a computer scientist either.

One general class of applications is to constructing true quotients, where you have a data structure in which the same "real object" has multiple representations; by representing it as a HIT you can add actual equalities between the two representations so that any function defined on this data structure must necessarily respect that equality (be "representation-independent").

Additionally, here are some posts from the homotopy type theory blog on topics that might be of interest to computer scientists:

• Abstract types with isomorphic types
• Higher lenses
• Homotopical patch theory
• HoTTSQL