Event Type:

Geometry-Topology Seminar

Date/Time:

Monday, April 18, 2022 - 12:00 to 12:50

Location:

BEXL 328 and Zoom

Local Speaker:

Abstract:

In the early 1900's, Bertrand Russell developed Type Theory as an alternate foundation of Mathematics in attempts to avoid paradoxes such as with the ``set of all sets''. Work with Type Theory laid dormant until the 1970's when Per Martin-L\"{o}f developed ``Dependent Type Theory'', a constructive theory which found it's way into theoretical computer science and eventually allowed for ``computer proof assistants''. It later, in the 1990's, became apparent that there were homotopical models in Dependent Type Theory that also existed in Category Theory. Then, in 2009, Vladimir Voevodsky championed the ``Univalence Axiom'' and began work on formalizing Dependent Type Theory from a homotopical viewpoint - Homotopy Type Theory was born. Since then, there has been much work done and the field has been developing very quickly! In this informal and introductory talk, I will give an overview of the basics of Homotopy Type Theory.