BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:An Authoritarian Approach to Presheaves - Pierre-M
arie Pédrot (INRIA)
DTSTART:20200605T130000Z
DTEND:20200605T140000Z
UID:TALK4233AT
URL:/talk/index/4233
DESCRIPTION:Presheaves are a well-known model of dependent typ
e theory.\nUnfortunately\, they are defined in a s
et-theoretic setting\, which makes\nthem not only
semantical objects\, but also silently relying on\
nextensionality principles. There have been a few
attempts at replacing\nset theory with type theory
as the target of this model construction\,\nresul
ting in what is called a syntactic model of type t
heory. Yet\, all\nthose constructions were subtly
flawed. The problem has been solved only\nvery rec
ently\, thanks to the introduction of a target typ
e theory\nextended with definitional proof irrelev
ance. I will recall the various\nattempts and thei
r issues\, and finally explain the recent result u
nder\nthe prism of programming language theory. Th
e latter model also makes\nsense in set theory\, a
nd constitutes a better behaved presentation of\np
resheaves\, in so far as it makes the resulting ca
tegory satisfy\ncomposition equations on the nose.
\n\nIf time permits\, I will also show how this te
chnique can be combined\nwith another syntactic mo
del\, known as the exceptional translation\, to\ne
xtended type theory with Markov's Principle while
retaining all good\ncomputational properties such
as canonicity\, strong normalization and\ndecidabi
lity of type-checking.
LOCATION:https://us02web.zoom.us/j/82603907326
CONTACT:Vincent Rahli
END:VEVENT
END:VCALENDAR