Mathematics and Computation

A blog about mathematics for computers

A course on homotopy (type) theory

This semester my colleague Jaka Smrekar and I are teaching a graduate course on homotopy theory and homotopy type theory. The first part was taught by Jaka and was a nice review of classical homotopy theory leading up to Quillen model categories. In the second part I am covering basic homotopy type theory.

The course materials are available at the GitHub repository homotopy-type-theory-course. The homotopy type theory lectures are also recorded on video.

Comments

Colin Paul Adams

Was the second half of the last lecture actually recorded?

Yes it was recorded and the video has now been fixed to include it. Sorry for the confusion!

Ivars

Thank you for publishing these.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.