## Abstract

Presheaf semantics [Hof97, HS97] 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) [AGJ14], univalent type theory (which is about preservation of equivalences) [BCH14, Hub15], directed type theory (which is about preservation of morphisms) and even combinations thereof [RS17, CH19]. 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 [Wad89] that follow from the preservation property concerned.

While the models for univalence, parametricity and directed type theory are all just cases of presheaf categories, approaches to internalize their results do not have an obvious common ancestor (neither historically nor mathematically). Cohen et al. [CCHM16] have used the final type extension operator Glue to prove univalence. In previous work with Vezzosi [NVD17], we used Glue and its dual, the initial type extension operator Weld, to internalize parametricity to some extent. Before, Bernardy, Coquand and Moulin [BCM15, Mou16] have internalized parametricity using completely different ‘boundary filling’ operators Ψ (for extending types) and Φ (for extending functions). Unfortunately, Ψ and Φ have so far only been proven sound with respect to substructural (affine-like) variables of representable types (such as the relational or homotopy interval I). More recently, Licata et al. [LOPS18] have exploited the fact that the homotopy interval I is atomic — meaning that the exponential functor (I→xy) has a right adjoint√— in order to construct a universe of Kan-fibrant types from a vanilla Hofmann-Streicher universe [HS97] internally.

A failed attempt to prove parametricity of System F in ParamDTT [NVD17] using Glue and Weld, set us on a quest to figure out what is the proper way to internalize presheaf semantics. A comparison of the expressive power of Glue, Weld, Φ, Ψ and a few additional operators, revealed that Φ cannot be implemented in terms of these other operators and strongly suggested that —in this set of operators — Φ is indispensible when it comes to proving parametricity of SystemF [ND18]. This is an unfortunate result, as our models of parametricity with identity extension [Nuy18] are incompatible with the substructurality of interval variables required by Φ and Ψ.

We propose a property that we will call dependable atomicity as a key notion to internalize presheaf semantics. Roughly speaking, we call a closed type I dependably atomic if the (potentially substructural) dependent function type former ((i:I)( xy) : Ty(Γ,i:I)→Ty(Γ) has a right adjoint (iG xy) : Ty(Γ)→Ty(Γ,i:I) which we will call the transpension. Dependable atomicity of I can be internalized using a transpension type former from which we can implement Ψ. Interestingly, this is feasible both in substructural and in cartesian settings.

All results presented below are preliminary; we are working on a proof assistant Menkar [ND19] in order to be able to trust our proofs.

While the models for univalence, parametricity and directed type theory are all just cases of presheaf categories, approaches to internalize their results do not have an obvious common ancestor (neither historically nor mathematically). Cohen et al. [CCHM16] have used the final type extension operator Glue to prove univalence. In previous work with Vezzosi [NVD17], we used Glue and its dual, the initial type extension operator Weld, to internalize parametricity to some extent. Before, Bernardy, Coquand and Moulin [BCM15, Mou16] have internalized parametricity using completely different ‘boundary filling’ operators Ψ (for extending types) and Φ (for extending functions). Unfortunately, Ψ and Φ have so far only been proven sound with respect to substructural (affine-like) variables of representable types (such as the relational or homotopy interval I). More recently, Licata et al. [LOPS18] have exploited the fact that the homotopy interval I is atomic — meaning that the exponential functor (I→xy) has a right adjoint√— in order to construct a universe of Kan-fibrant types from a vanilla Hofmann-Streicher universe [HS97] internally.

A failed attempt to prove parametricity of System F in ParamDTT [NVD17] using Glue and Weld, set us on a quest to figure out what is the proper way to internalize presheaf semantics. A comparison of the expressive power of Glue, Weld, Φ, Ψ and a few additional operators, revealed that Φ cannot be implemented in terms of these other operators and strongly suggested that —in this set of operators — Φ is indispensible when it comes to proving parametricity of SystemF [ND18]. This is an unfortunate result, as our models of parametricity with identity extension [Nuy18] are incompatible with the substructurality of interval variables required by Φ and Ψ.

We propose a property that we will call dependable atomicity as a key notion to internalize presheaf semantics. Roughly speaking, we call a closed type I dependably atomic if the (potentially substructural) dependent function type former ((i:I)( xy) : Ty(Γ,i:I)→Ty(Γ) has a right adjoint (iG xy) : Ty(Γ)→Ty(Γ,i:I) which we will call the transpension. Dependable atomicity of I can be internalized using a transpension type former from which we can implement Ψ. Interestingly, this is feasible both in substructural and in cartesian settings.

All results presented below are preliminary; we are working on a proof assistant Menkar [ND19] in order to be able to trust our proofs.

Original language | English |
---|---|

Publication status | Published - 14 Jun 2019 |

Event | International Conference on Types for Proofs and Programs - Oslo, Norway Duration: 11 Jun 2019 → 14 Jun 2019 Conference number: 25 https://cas.oslo.no/types2019/ |

### Conference

Conference | International Conference on Types for Proofs and Programs |
---|---|

Abbreviated title | TYPES |

Country | Norway |

City | Oslo |

Period | 11/06/19 → 14/06/19 |

Internet address |