University of Cambridge > > Category Theory Seminar > Homotopy Type Theory and Univalent Foundations of Mathematics II

Homotopy Type Theory and Univalent Foundations of Mathematics II

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2019, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity