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.
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.
In addition, experience with proof assistants and dependently typed programming would be really useful.