University of Birmingham > Talks@bham > Theoretical computer science seminar > Types are Internal oo-Groupoids

Types are Internal oo-Groupoids

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

If you have a question about this talk, please contact Martin Escardo.

With the introduction of Homotopy Type Theory, it has become clear that a constructive, proof-relevant interpretation of equality endows types with and extremely rich algebraic structure. In classical mathematics, this structure is well-known under the name “oo-groupoid” and was originally proposed by Grothendieck as a model for the notion of homotopy type which arises naturally in algebraic topology.

By now there are a number of meta-theoretic results which firmly establish a connection between known definitions of oo-groupoid and models of type theory. However, a natural question which remains unanswered is the following: can we describe the notion of oo-groupoid using type theory itself? And furthermore, can we show, internally to the theory, that all types indeed carry this structure?

While a complete answer to the above questions remains elusive, I will present in this talk a way of extending type theory with certain new primitives which allow us to express the desired structure and to prove a strong form of the statement that types carry the structure of oo-groupoids: specifically, that they type of all oo-groupoids is in fact equivalent to the universe of types itself.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.