Homotopy Theory Topics Seminar

The theory of types was introduced by Bertrand Russell as a foundation for mathematics that avoids Russell's paradox. A more refined theory was introduced by Martin-Löf in 1972, and this theory is the basis for much modern research on type theory. It was later realized that type theory also has an intrinsically homotopical interpretation, and describing this will be the long term goal of the seminar series.

In this talk, I will give an introduction to (non-homotopical) type theory, explaining how types can be thought of either as sets or as propositions, and give examples of how to do mathematics using type theory. I will also show how type theory is used in the proof assistant Coq, which has been used to formalize many non-trivial results. I will also discuss the intuitionistic logic that arises in type theory.

We will discuss inductive types, which are defined using constructors. Examples include the unit type, sum types, and product types introduced last week. Then we will discuss proofs by induction in the context of inductive types. Lastly, we will discuss identity types, which will play the role of path spaces in the homotopical interpretation of type theory.

After recalling the construction of identity types as inductive types, we will use the induction principle to prove basic facts about identity types. Throughout the talk, we will pursue the analogy between identity types and path spaces. We will illustrate how iterated identity types form a structure reminiscent of the low-dimensional data of an $\infty$-groupoid.

We will continue the discussion of path induction, and use it to produce further operations on paths, such as applying functions to paths, and the transport between fibers. Then, we will discuss the notions of homotopy between functions and equivalence between types.

I will describe what it means to give a model of type theory, and give some examples of models, including some that arise from Quillen model categories.