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…