Dan Christensen, Western University
"An introduction to homotopy type theory"
Type theory is a formal system that was originally intended to describe set-like objects, and which is well-suited to formalizing proofs so that they can be verified by a computer. Recently, it was realized that type theory is intrinsically homotopical, and can be used to reason about spaces and other homotopical categories. Voevodsky introduced the univalence axiom, which says roughly that homotopy equivalence and equality agree, and implies many homotopical results. This talk will start with an introduction to type theory, will introduce univalence and give examples of its consequences. No background in type theory or homotopy theory will be assumed.
MC 5501