Homotopy Type Theory Seminar

Andrej Vukovic, Department of Pure Mathematics, University of Waterloo

"Homotopy Type Theory and Univalent Foundations"

Homotopy type theory is a rapidly developing area of mathematics that unifies ideas from logic (namely Martin-Lof type theory) with ideas from topology and homotopy theory. In our first talk, we motivate homotopy type theory by contrasting it with other foundational areas of mathematics (e.g., set theory, category theory). We introduce Martin-Lof type theory and function types. We conclude by discussing the importance of the univalence axiom.

MC 5413