Type theory and homotopy

TL;DR

This survey explores the emerging connection between type theory, homotopy theory, and higher-dimensional categories, highlighting recent interpretative advances linking logic, geometry, and algebra.

Contribution

It introduces the interpretation of Martin-Löf's constructive type theory into homotopy theory, providing new insights and examples of higher-dimensional categories.

Findings

Link between constructive type theory and homotopy theory established

New examples of higher-dimensional categories presented

Bridges between logic, geometry, and algebra highlighted

Abstract

The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Martin-L\"of into homotopy theory, resulting in new examples of higher-dimensional categories.