Till innehåll på sidan

Simon Henry: Constructive homotopy theory, Weak model structures and infinity groupoids in type theory

Tid: On 2018-02-28 kl 10.00 - 11.45

Plats: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University 

Medverkande: Simon Henry, Masaryk University, Brno

Exportera till kalender

Abstract: This talk will be about two closely related topics:

In the first part I will introduce a notion of "weak model structure". It is a weakening of the notion of Quillen model structure, which still allows to carry most of usual homotopy theory. These weaker structure appear to be considerably easier to construct than Quillen model structures, so much so that it will be possible to get rather directly 'weak' analogue of most classical model structures, in constructive and even predicative mathematics. This includes things like the Quillen model structure on simplicial sets, the model structure for quasi-categories, chain complexes, cubical sets, dendroidal sets, the folk model structure on infinity category, and lots of other examples...

In the second part, I will present some new tools to construct and compare concrete models for the notion of infinity groupoids. These tools will have two interesting applications:

They allow to construct a new notion of infinity groupoids which:
- use a globular combinatorics.
- can be defined within homotopy type theory.
- can be proved (in classical mathematics, or even constructively) to be equivalent to other notions of infinity groupoids, like Kan complexes.

These tools also shows that similarly to how every type in type theory has a structure of Batanin (or Grothendieck) infinity groupoid, it also has a structure of Kan complexe. In particular, to any type in any intentional type theory one can attach naturally a topological space with the same homotopy groups as the type.