Was soll HoTT?

Description

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.

This the the first (or, rather, zeroth) video in a planned video series covering the basics of homotopy type theory. This is a reboot of the video series I started last year (Old Intro to HoTT)—I got too busy last year with teaching and starting my PhD. Thanks to everyone who left kind comments on those videos, and encouraged me to make videos again!

Pardon my butchering of the German language.

Some relevant resources:

• Article about Mochizuki’s purported proof of the ABC conjecture
• Lean theorem prover
• Good post describing more about different kinds of typing. When I speak of “typed programming languages”, I actually mean strong, statically-typed programming languages. Python isn’t truly untyped—it actually has a type system—but not a strong, static one like I describe here.
• Resources page for Egbert Rijke’s Introduction to Homotopy Type Theory textbook
• Gauss kindergarten formula

Formalization links:

• The formalization I’m developing for this video series

HoTT textbooks:

• The HoTT Book (2013)—the original statement of HoTT
• Introduction to Homotopy Type Theory, by Egbert Rijke (to be released)