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