When: Thursday, February 04, 1:00 p.m.- 2:30 p.m.

Where: 6115 Gates & Hillman Centers

Vladimir Voevodsky ,
Professor of Mathematics
Institute for Advanced Study
Princeton University

POP Seminar

Abstract:
I will show how to define, in any type system with dependent sums, products and Martin-Löf identity types, the notion of a homotopy equivalence between two types and how to formulate the Equivalence Axiom which provides a natural way to assert that “two homotopy equivalent types are equal”. I will then sketch a construction of a model of one of the standard Martin-Löf type theories which satisfies the equivalence axiom and the excluded middle thus proving that M.L. type theory with excluded middle and equivalence axiom is at least as consistent as ZFC theory. Models which satisfy the equivalence axiom are called univalent. This is a totally new class of modes and I will argue that the semantics which they provide leads to the first satisfactory approach to type-theoretic formalization of mathematics.

Vladimir Voevodsky is a professor of mathematics at the Institute for Advanced Study in Princeton. He is best known for the development of the motivic homotopy theory and for the proof of Milnor’s conjecture which earned him the Fields Medal in 2002. He studied mathematics in Moscow University and received his Ph.D. from Harvard in 1992.

Faculty Host: Robert Harper
Appointments: kmm@cs.cmu.edu

<< Back