The new subject of "homotopy type theory" has been created by a fusion of homotopy theory, higher category theory, and constructive type theory. On one hand, it enables us to apply homotopical ideas in type theory, giving new ways to deal with things like proof-irrelevance, singleton elimination, type equivalence, and universes. On the other hand, it gives us a formal language in which to do homotopy theory. A proof written in this language will automatically be valid in many different "homotopy theories", and can also be formalized and checked by a computer proof assistant. Taken to an extreme, the subject offers the possibility of a new foundation for mathematics in which the basic objects are homotopy types, rather than sets. References can be found at the Homotopy type theory web site.
This weekly seminar will be an introduction to the subject and some of its highlights, assuming no background in either homotopy theory or type theory. In addition to the mathematical theory, we will learn to formalize it using the computer proof assistant Coq.
The seminar meets from 10:30 – 12:00 on Tuesdays in AP&M 5402.
This talk will be a high-level overview of type theory, homotopy theory, and the connection between the two. No background will be assumed, and nothing will be very precise.
This will be an introduction to the formal syntax and rules of type theory. We will work with "pure type systems" (augmented by inductive types) as a simple, but sufficiently general, framework. In parallel with the mathematical theory, we will start learning how to formalize type theory in Coq and use it as a programming language.
We will discuss inductive types, inductive families, programming with recursive functions, and the distinction between parameters and indices. Inductive types are the basic way to define positive types in Coq. Then we will define identity types (a.k.a. equality types or path types) as inductive families.
The seminar will resume on February 21.
We will now begin working with homotopical types. We'll talk about operations on paths and what the path spaces of different types look like. Then we'll focus on the embedding of logic into homotopy type theory with "h-propositions", which will provide a basic grounding for developing mathematics. Then we'll define the tower of homotopy levels, and survey the many ways to define "equivalences" in homotopy type theory. If time permits, we will state the univalence axiom.
We'll discuss the correspondence between type theory (syntax) and category theory (semantics), starting with simply typed lambda calculus and then moving on to dependent type theory. In particular, we'll talk about how type constructors correspond to objects with universal properties in category theory. We'll use display maps to represent dependent types categorically, and we'll see that in homotopy theory the display maps have to be fibrations.
Switching gears, we'll spend a while on abstract homotopy theory, represented using weak factorization systems and model categories. Then we'll see how this structure is exactly what we need in order to interpret intensional dependent type theory.
We'll end by discussing higher inductive types, a way to build familiar spaces and homotopy-theoretic constructions in type theory using a syntax that generalizes traditional type-theoretic inductive definitions. In particular, we can define circles and sphere, calculate some homotopy groups, define truncations and localizations, and build the "other half" of a model category structure, completing the correspondence between type theory and abstract homotopy theory.