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 - 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. |
## Other listsVirtual Harmonic Analysis Seminar MaterialWell Computer Science Lunch Time Talk Series## Other talksSylow branching coefficients for symmetric groups TBC Modelling uncertainty in image analysis. Ultrafast, all-optical, and highly efficient imaging of molecular chirality Geometry of alternating projections in metric spaces with bounded curvature Quantum simulations using ultra cold ytterbium |