[stepchowfun]

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]

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]

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.