Title: Type theory and homotopy theory
Speaker: Paige North (The Ohio State University)
Abstract: Martin-Löf type theory is an alternative foundation of mathematics invented in the 1970s. It is the mathematical language used by computer proof checkers such as Coq and Agda. One peculiar feature of this language is that its notion of equality is much weaker than the normal mathematical notion of equality.
In the early 2000s, it was realized that the rules for this equality describe some kind of homotopy theory. In particular, these rules look a lot like some of the axioms for a Quillen model structure. These observations have grown into a research program called Homotopy Type Theory.
In this talk, I will describe the basics of Martin-Löf type theory, the basics of Quillen model structures, and the connection between these two.
Note: The goal of Welcome Seminar is to give an opportunity to new postdoctoral fellows and tenure track professors to introduce themselves to their colleagues. The talks are intended to be non-technical and accessible to graduate students as well. Please plan to attend and encourage your graduate students to do so as well. The talk will be preceded by a colloquium-style reception at 4:00, in the area adjacent to Cockins Hall 240 on the second floor of the Math Building.