Lambda Jam 2014 Gershom Bazerman Homotopy Type Theory: Whats the Big Idea

Homotopy Type Theory is a research program that brings together computer science (in the form of dependent type theory), logic, and algebraic topology in a single cohesive way. Its great insight is in systematizing the way in which these fields have all, in some sense been studying the same thing. From the standpoint of computer science, it consists of a new geometric interpretation of dependent type theory in which we think of types as topological spaces, and also the a