COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## Homotopy Type Theory and Univalent Foundations of Mathematics IIAdd 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
- MR13, Centre for Mathematical Sciences
- School of Physical Sciences
- bld31
- ndb35's list
Note that ex-directory lists are not shown. |
## Other listsSeminar on Religion, Conflict and Its Aftermath Dying Planet, Living Faith: Religious Contributions to Environmentalism Clare Politics## Other talksDynamical large deviations in glassy systems Recent Changes of Korean Government's Strategy on back-end fuel cycle and the changing course of a University Laboratory Frontiers in paediatric cancer research Responsible Research and Innovation Lunch- Lent 2018 The Exposome in Epidemiological Practice TODAY Adrian Seminar: "Starting new actions and learning from it" |