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

An Authoritarian Approach to Presheaves

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

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.