Hacker News Reader

I'm curious what the pre-requisites for this course would be. I don't see it listed anywhere on that page, but I do see intuitionist prepositional logic listed as a topic for classes early in the semester. Other than that, what other topics would help build up a good base for Homotopy Type Theory?

View on HN

It isn't strictly required, but a background in algebraic topology is really useful for understanding the homotopy bit. That has point-set topology and abstract algebra as pre-reqs. Abstract algebra is a very useful tool for reasoning about computing in its own right.

In addition, experience with proof assistants and dependently typed programming would be really useful.

Great response, thank you!

Dr. Harper suggested that abstract topology isn't such a requirement as they'll develop it synthetically in the class. Then algebraic topology as it's usually developed will become a useful metaphor.

Dr. Harper spends a lot of time developing IPL and it's semantics both as Heyting Algebra and a Bi-Cartesian Closed Category in the first few weeks. I found it easy to follow with a smattering of type theory and category theory background.

Reply on news.ycombinator.com