Homotopy Type Theory and Univalent Foundations of Mathematics II

Add to your list(s) Download to your calendar using vCal

• Chris Kapulkin, University of Pittsburgh
• Wednesday 29 June 2011, 14:15-15:15
• MR13, Centre for Mathematical Sciences.

If you have a question about this talk, please contact Nathan Bowler.

This series of talks is an introduction to Homotopy Type Theory and the Univalent Foundations of Mathematics. This new area of research develops a beautiful connection between algebraic topology (homotopy theory) and theoretical computer science (type theory).

The second talk will serve an introduction to the Univalent Foundations. This program started by Vladimir Voevodsky (IAS, Princeton) provides new interesting foundations of mathematics (based on type theory), naturally formalizing categorical and higher-categorical thinking. The main purpose of this project is to have a language based on homotopy types (as opposed to sets) that would enable one to easily prove results from homotopy theory using a proof assistant such as Coq. This can be accomplished by adding the Univalence Axiom to the standard set of rules of type theory. In the talk we will discuss the Univalence Axiom together with some of its basic consequences, higher inductive types, and a type theoretic proof of $\pi_1 (S^1) = \mathbb{Z}$.

This talk is part of the Category Theory Seminar series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Category Theory Seminar
• DPMMS Lists
• DPMMS Pure Maths Seminar
• DPMMS info aggregator
• DPMMS lists
• Hanchen DaDaDash
• Interested Talks
• MR13, Centre for Mathematical Sciences
• School of Physical Sciences
• bld31
• ndb35's list
• yk373's list

Note that ex-directory lists are not shown.