Guillaume Brunerie: A type-theoretic definition of weak infinity-groupoids

The notion of weak infinity-groupoid was originally developed by Grothendieck with the hope of providing an algebraic model for spaces up to homotopy. This notion has also recently come up in type theory with the proof by van den Berg, Garner and Lumsdaine that every type in dependent type theory has the structure of a weak infinity-groupoid (using the definition of Batanin-Leinster). In this talk I will present a type-theoretic definition of the notion of weak infinity-groupoid, equivalent to Grothendieck’s definition, and prove that every type in dependent type theory is such a weak infinity-groupoid.