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