Homotopy Type Theory

Student Colloquium

Homotopy type theory is a new branch of mathematics that combines and connects aspects of several different fields (topology, logic, category theory, etc.) in surprising ways. Briefly, logical constructions correspond to homotopy-invariant constructions on spaces, while theorems and proofs in the logical system are given a homotopical meaning.

In the colloquium we will aim to give the audience an introduction to the ideas, methods and results of the ongoing work in this area.

The colloquium will consist of two talks with a break in the middle. The talks will be accessible to second year students who have seen some topology (in particular the notion of a homotopy between paths) but anyone interested is welcome!