An Authoritarian Approach to Presheaves

Add 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.