Three for One: Homotopy Interpretation

Description

What does homotopy type theory mean? This video presents the next answer: HoTT is a language for describing spaces. Under this interpretation, the unit type 1 represents the space consisting of just a single point. This video informally introduces the idea of "contractibility", which we'll rigorously define later and use extensively throughout HoTT.

• Part 0
• Part 1
• Part 3

Further Reading

• Numberphile has several excellent videos on Klein Bottles, e.g. this one
• SEP article on Set Theory

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)