![]() |
![]() |
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
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:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here Facts and Snacks Speech Recognition by Synthesis SeminarsOther talksLife : it’s out there, but what and why ? Hunt for an Earth-twin TBA Counting cycles in planar graphs Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy Ultrafast Spectroscopy and Microscopy as probes of Energy Materials |