Three for One: Programming Interpretation

Description

What does homotopy type theory mean? This video presents the first answer: HoTT is a typed programming language. Under this interpretation, the unit type 1 is the type of zero-tuples, a standard feature in many typed programming languages.

• Part 0
• Part 2
• Part 3

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)