# Groupoids and ∞-groupoids in type theory

**Date**: Wednesday 27 September 2017, 16:00 – 17:00**Location**: Mathematics**Type**: Logic, Seminars, Pure Mathematics**Cost**: Free

#### 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*