Three for One: Introduction

Description

What does homotopy type theory mean? This is a question which has three distinct answers, connecting the language of HoTT to the rich worlds of functional programming, homotopy theory, and constructive logic.

• Part 1
• Part 2
• Part 3

Further reading:

• Blog by Bob Harper about computational trinitarianism
• nLab page

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)