Pierre-Marie Pédrot
Gallinette Team, Inria Rennes-Bretagne-Atlantique
All your base categories are belong to us: A syntactic model of presheaves in type theory
Presheaves are a staple categorical structure, which naturally arises in a wide variety of situations. In the realm of logic, they are often used as a model factory. Indeed, presheaves over some base category will result in a topos, whose contents can be fine-tuned by carefully picking the base category. As computer scientists, though, we have learnt that there are even better logical systems than toposes: dependent type theories! Through the Curry-Howard mirror, they are also full-blown functional programming languages that actually compute.
This begs the following question: is it possible to build the type-theoretic equivalent of presheaves, while retaining the good computational properties of our dependent programming languages? We will see that strikingly enough, presheaves can already be presented as computational objects to some extent, except for the annoying fact that they do not obey the right conversion rules! A proper account of type-theoretic presheaves will require a coming-of-age journey through the world of effectful program semantics, using fine and modern tools such as call-by-push-value, dependent parametricity and strict equality. In the end, we will formulate an alternative presentation of presheaves in type theory, but which is still equivalent to its standard categorical counterpart when viewed from the static world of sets. As an application, we will use them to extend dependent type theory with new effective logical principles.
Chair: Paul Blain Levy
Event Timeslots (1)
Friday
-
by Pierre-Marie Pédrot
Leave a Comment