Xoltar

Higher Order Type Theory Resources

Recently there’s been an outpouring of useful resources folks have found for learning Homotopy Type Theory (aka HoTT). These have come mainly from the HoTT Cafe Google Group.

The main resource is of course, the book, but these videos and other resources seem useful enough that I want a consolidated list of them for myself. So I thought maybe you might, too.

Group threads that provided these links:

• Long way to the HoTT book
• HoTT without homotopy?
• Robert Harper’s HoTT course at CMU

Note that I’m likely to update this page in the future with other resources as I find them, and those links may or may not come from the Groups threads just mentioned.

Useful resources, in no particular order:

• Univalence as a new Principle of Logic - recommended by one writer as perhaps the first video to watch
• Wadler’s Propositions as Types paper - recommended by one writer as a good pairing with chapter 1 of the hott book.
• Robert Harper’s 15-819 Homotopy Type Theory(videos
• Awodey’s Category Theory book
• Awodey’s Category Theory lecture videos (URL is to first video, it’s a series)
• Bristol HoTT project

Related:

• Cubical models in Haskell
• Cubical type theory implementation
• Possible pre-hott intro material - course material, author mentions it may be hard to follow as a standalone resource
• Structural set theory