Homotopy Theory Topics Seminar

I will give an overview of the field of Homotopy Type Theory. This relatively new field of mathematics is based on a realization that the formal logical system of dependent type theory can be interpreted in various homotopy-theoretic settings. After briefly discussing type theory, I will sketch the idea of its homotopical interpretation and its connection to higher category theory. In the last part of the talk, I will highlight some recent results.

We will discuss in more detail the rules that define types, along with examples. The focus will be on inductive types, which are characterized by their constructors. An important example of inductive types is given by identity types, which play the role of path spaces in the homotopical interpretation. We will discuss path induction and the higher groupoid structure obtained from iterated identity types.

We will introduce the Univalence Axiom and discuss a few of its immediate consequences such as existence of types that are not sets, function extensionality, or preservation of n-types by dependent products.

Higher inductive types are a generalization of inductive types. While an inductive type is generated by certain terms, a higher inductive type may be generated by terms, paths between terms, paths between paths between terms, etc. In the homotopy theoretic model of type theory, this corresponds to constructing cell complexes. We will see many other uses of higher inductive types, and will sketch the argument that $\pi_1(S^1)$ is isomorphic to the integers.

I'll discuss the notion of a model of dependent type theory. After outlining the general algebraic semantics, I'll show how such models can be constructed from categories that we encounter in the so-called "mathematical practice".

In this talk, we will show a way to develop category theory in Univalent foundations. As it turns out, the naive reformulation of the standard axioms from set theory leads to a rather ill-behaved notion. We show how it can be refined. We also observe that for these redefined categories, two concepts of equivalence and isomorphism are the same.

I will talk about homotopy type theoretic proofs of a well known topological fact that the fundamental group of the circle is the set of integers. There are two closely related proofs. The homotopy-theoretic proof follows a similar reasoning used in the classical proof in topology, whereas the encode-decode proof is more type theoretic.

We introduce fiber sequences and the Hopf fibration $S^3 \to S^2$ in HoTT, and we show that the Hopf fibration induces equivalences between the homotopy groups $\pi_k$ of $S^3$ and $S^2$ for $k>2$. We also deduce that $\pi_2(S^2)$ is equivalent to $Z$. We will review the background on truncations and connectedness in this talk too.

I will present a proof of the Freudenthal suspension theorem in HoTT. Unlike many other proofs in HoTT, this one is not merely an adaptation of a classical argument, but involves genuinely new techniques.

We will review the notion of model of dependent type theory, with prescribed constructors. Then we will describe work of Kapulkin, Lumsdaine, and Voevodsky producing a model in the category of simplicial sets, for which the Univalence Axiom holds.