Andreas Nuyts ; Dominique Devriese - Transpension: The Right Adjoint to the Pi-type

lmcs:6725 - Logical Methods in Computer Science, June 19, 2024, Volume 20, Issue 2 - https://doi.org/10.46298/lmcs-20(2:16)2024
Transpension: The Right Adjoint to the Pi-typeArticle

Authors: Andreas Nuyts ; Dominique Devriese

    Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to make the resulting language more expressive, or in order to carry out further reasoning internally, allowing greater abstraction and sometimes automated verification. While the constructions of presheaf models largely follow a common pattern, approaches towards internalization do not. Throughout the literature, various internal presheaf operators ($\surd$, $\Phi/\mathsf{extent}$, $\Psi/\mathsf{Gel}$, $\mathsf{Glue}$, $\mathsf{Weld}$, $\mathsf{mill}$, the strictness axiom and locally fresh names) can be found and little is known about their relative expressivenes. Moreover, some of these require that variables whose type is a shape (representable presheaf, e.g. an interval) be used affinely. We propose a novel type former, the transpension type, which is right adjoint to universal quantification over a shape. Its structure resembles a dependent version of the suspension type in HoTT. We give general typing rules and a presheaf semantics in terms of base category functors dubbed multipliers. Structural rules for shape variables and certain aspects of the transpension type depend on characteristics of the multiplier. We demonstrate how the transpension type and the strictness axiom can be combined to implement all and improve some of the aforementioned internalization operators (without formal claim in the case of locally fresh names).


    Volume: Volume 20, Issue 2
    Published on: June 19, 2024
    Accepted on: April 15, 2024
    Submitted on: August 21, 2020
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 759 times.
    This article's PDF has been downloaded 157 times.