Tags:dependent type theory, internal parametricity, presheaf models and proof of univalence
Abstract:
Presheaf semantics are an excellent tool for modelling relational preservation properties of (dependent) type theory. They have been applied to parametricity (which is about preservation of relations), univalent type theory (which is about preservation of equivalences), and directed type theory (which is about preservation of morphisms). Of course after going through the endeavour of constructing a presheaf model of type theory, we want type-theoretic profit, i.e. we want internal operations that allow us to write cheap proofs of the 'free' theorems that follow from the preservation property concerned. There is currently no general theory of how we should craft such operations. Cohen et al. introduced the final type extension operation Glue, using which one can prove the univalence axiom and hence also the 'free' equivalence theorems it entails. In previous work with Vezzosi, we showed that Glue and its dual, the initial type extension operation Weld, can be used to internalize parametricity to some extent. Earlier, Bernardy, Coquand and Moulin had introduced completely different 'boundary-filling' operations to internalize parametricity. Each of these operations has to our knowledge only been used in concrete models and hence their expressivity has not been compared. We have done some work to fill the hiatus: we consider and compare the various operators in more general presheaf categories. In this first step, we do not consider fibrancy requirements.
Internalizing Presheaf Semantics: Charting the Design Space