Was soll HoTT? [Intro to HoTT, No. 0]

Links and more: https://intro-hott.video/videos/0

What is homotopy type theory good for? In this video, I discuss the ideas of type-checking and formalized mathematics, and begin to describe how HoTT promises a new future for mathematics.

Video site for the series: https://intro-hott.video
Youtube:    • Intro to Homotopy Type Theory  
Instagram:   / intro_hott  


Homotopy type theory (HoTT) is a new branch of type theory and a new foundation for mathematics. It serves as a common language for reasoning about computation (functional programming), about mathematical structure (synthetic homotopy theory and higher category theory), and about constructive logic. This Introduction to Homotopy Type Theory video lecture series is intended to explain what HoTT is, show how to work in HoTT (including how formalization in Agda works), and give intuition for why HoTT is the way it is. I don’t assume any particular background familiarity, but the more you know about mathematics, computer science, and logic, the more you’ll be able to get out of these videos. Enjoy!

00:00 - 01:49: Intro
01:49 - 03:00: Welcome
03:00 - 05:51: A problem with proof-reading
05:51 - 16:35: The art of typechecking
16:35 - 25:27: Remaking math in type theory's image