Post date: 02-sep-2015 13:48:17
It is conjectured that intensional dependent type theory (with some standard type constructors) plus the univalence axiom is the internal language for ∞-topoi. The goal of this talk is to motivate the idea that HoTT is the logic of homotopy types, in the same way that extensional type theory can be interpreted as the logic of sets, standard intuitionistic logic.
We will start by defining some basic types and type constructors, pointing out their categorical properties. We will use them to make classic constructions in homotopy theory and to prove some of their properties. We will see that we are able to work with these objects directly, without needing some kind of presentation, like CW-complexes or simplicial sets. So, in some sense, we will be able to work with "the" ∞-category of homotopy types directly, without presenting it in some indirect way.
Just to give some idea of the kind of calculations that are possible in this setting, we will define the homotopy groups of a type, and the cohomology of a type (with coefficients in some other type, or more gerenerally, a type spectrum). We will see that the standard properties (like the long exact sequences of a fibration and cofibration repectively) hold in this setting.