University of Birmingham > Talks@bham > Theoretical computer science seminar > An Authoritarian Approach to Presheaves

## An Authoritarian Approach to PresheavesAdd to your list(s) Download to your calendar using vCal - Pierre-Marie Pédrot (INRIA)
- Friday 05 June 2020, 14:00-15:00
- https://us02web.zoom.us/j/82603907326.
If you have a question about this talk, please contact Vincent Rahli. Presheaves are a well-known model of dependent type theory. Unfortunately, they are defined in a set-theoretic setting, which makes them not only semantical objects, but also silently relying on extensionality principles. There have been a few attempts at replacing set theory with type theory as the target of this model construction, resulting in what is called a syntactic model of type theory. Yet, all those constructions were subtly flawed. The problem has been solved only very recently, thanks to the introduction of a target type theory extended with definitional proof irrelevance. I will recall the various attempts and their issues, and finally explain the recent result under the prism of programming language theory. The latter model also makes sense in set theory, and constitutes a better behaved presentation of presheaves, in so far as it makes the resulting category satisfy composition equations on the nose. If time permits, I will also show how this technique can be combined with another syntactic model, known as the exceptional translation, to extended type theory with Markov’s Principle while retaining all good computational properties such as canonicity, strong normalization and decidability of type-checking. 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
- Theoretical computer science seminar
- computer sience
- https://us02web.zoom.us/j/82603907326
Note that ex-directory lists are not shown. |
## Other listsBritGrav 15 Centre for Computational Biology Seminar Series Jane Langdale## Other talksTBA The science of the large scale heliosphere and the missions that made it possible TBC Plasmonic Electronic Paper Structured Decompositions: recursive data and recursive algorithms [Colloquium:] Aperture Fever: The Extremely Large Telescope |