9 ms·

I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and comp

I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and computer scientists. I think a "homotopy type theory for programmers" book/blog/playlist could be a big hit. I've been considering putting something like that together. I view the relationship between HoTT and topology as similar to that of functional programming and category theory: you don't need to know the latter to learn the former, but having that extra background can certainly help.

isaac21259 4y ago
I was also considering writing some introductory stuff about HoTT but I don't think it's possible to avoid talking about topology, homotopy theory, and category theory in depth like you can with, say Haskell and category theory. This is because the stuff that makes HoTT so cool cannot be separated from it's mathematical foundations. How would you explain truncated types without going fairly deep into the math? Or the circle type? Sure both of these could be explained as instances of higher inductive types but that explanation is missing a lot.
- Koshkin 4y ago
  As already has been done with category theory, you need to target a specific audience, whether it is programmers, scientists, engineers, or mathematicians, and illustrate the concepts by giving examples from their area of expertise, if possible.
deleted 4y ago
[deleted]