Groupoids and ∞-groupoids in type theory

Nicola Gambino, University of Leeds. Part of the mathematics logic seminars series.

A groupoid is a category in which every morphism is invertible. Examples of groupoids abound throughout mathematics; for example, every topological space has a fundamental groupoid, consisting of points and homotopy classes of paths. In mathematical logic, groupoids provided the first example of a model of Martin-Löf type theory in which identity types were not interpreted trivially. More recently, ∞-groupoids have been considered as models of Martin-Löf type theory extended with Voevodsky’s univalence axiom. The aim of the talk will be to explain what groupoids and ∞-groupoids are, survey their applications to type theory, including some joint work with Christian Sattler attempting to define a constructive model of the univalence axiom with ∞ groupoids.

Nicola Gambino, University of Leeds