11 ms·
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
by ddellacosta 13y ago
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?
- chas 13y agoIt 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.
- ddellacosta 13y agoGreat response, thank you!
- tel 13y agoDr. 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.
- tel 13y agoDr. 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.