# Higher inductive type: what for?

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?

• Just to amend Mike's answer, Thorsten Altenkirch has some applications of HITs to the theory of containers. – Ingo Blechschmidt Mar 18 at 22:21

• Assuming a type A and an equivalence relation R : A -> A -> Prop, how would you define the HIT A/R that is the true quotient of A by R? – Bob Mar 18 at 19:39
• A constructor [-] : A -> A/R, a constructor forall (x y : A), R x y -> [x] = [y], and probably a 0-truncation constructor forall (x y : A/R) (p q : x = y), p = q. See section 6.10 in the HoTT Book. – Mike Shulman Mar 18 at 21:08