![]() |
![]() |
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 Filling in the blank – I will be ….... in 2050’ Type the title of a new list hereOther talksSignatures of structural criticality and universality in the cellular anatomy of the brain The percolating cluster is invisible to image recognition with deep learning Seminar [Seminar]: Two easy three-body problems Towards Efficient and Robust Data-Driven Optimization [Friday seminar]: Irradiated brown dwarfs in the desert |