# A course on homotopy (type) theory

- 08 May 2019
- Type theory, Teaching

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.

##### Post a comment:

Write your comment using Markdown.
Use

`$⋯$`

for inline and `$$⋯$$`

for display LaTeX formulas,
and `<pre>⋯</pre>`

for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.
## Comments

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!

Thank you for publishing these.