![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Types are Internal oo-Groupoids
![]() Types are Internal oo-GroupoidsAdd to your list(s) Download to your calendar using vCal
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:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here Applied Mathematics Seminar Series Electromagnetic Communications and Sensing Research Seminar SeriesOther talksHunt for an Earth-twin Counting cycles in planar graphs Quantum Sensing in Space TBA TBA Wave turbulence in the Schrödinger-Helmholtz equation |