Types are Internal oo-Groupoids

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

• Eric Finster, School of Computer Science, University of Birmingham
• Friday 24 September 2021, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

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

https://bham-ac-uk.zoom.us/j/83662748860?pwd=dTBRV1JCUEgxQXV1cXpjV3pDaGttUT09

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.

https://bham-ac-uk.zoom.us/j/83662748860?pwd=dTBRV1JCUEgxQXV1cXpjV3pDaGttUT09

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

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.