[ebingdom]

> I do not understand why homotopy type theory posts are so popular on this website.

Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming language that is capable of expressing both programs and proofs, such that you can prove your code correct in the same language. Hacker News is a mostly technical community that often likes to geek out on programming languages.

Homotopy type theory is an especially cool flavor of type theory that finally gives a satisfying answer to the question of when two types should be considered propositionally equal.

[thechao]

> finally gives a satisfying answer to the question of when two types should be considered propositionally equal

One of my fondest memories was listening to Walid Taha debate Jeremy Siek, Todd Veldhuizen, and others, over beers, about the best way to define type equivalence in nontrivial type systems. It seemed so abstract, until I had to debug a template instantiation issue in GCC.

[hash-no-gal-fld]

I don't think you intended "propositionally" equal in your final sentence. Equality is data in HoTT. If you take the propositional truncation then you usually throw away too much.

[ebingdom]

Yeah, I only meant as opposed to judgmental equality, not the quality of being a proposition.