Transpension: The Right Adjoint to the Pi-type
Andreas Nuyts, Dominique Devriese
TL;DR
This work introduces transpension, a right adjoint to shape-quantified universal quantification, as a unifying primitive for internalizing presheaf-model constructions within dependent type theory. Building a general multimodal framework MTraS (with shape contexts and endofunctor multipliers), the paper derives a coherent semantics and shows how a broad class of internal operators (including Phi, Psi, Glue, Weld, mill, and locally fresh names) can be recovered from transpension together with a strictness axiom and certain pushouts. It provides a Fully Faithful FFTraS instantiation to illustrate the core ideas before deploying MTraS to encompass substitution, weakening, and Cartesian multipliers, and then revisits FFTraS to demonstrate a pseudo-embedding. The results enable auto-internal reasoning about fibrancy and presheaf-like structures in a wide range of base categories, with explicit mechanisms for higher-dimensional pattern matching and boundary analysis. Collectively, this framework advances internal hardening of presheaf models, reduces the operator zoo to a small set of primitives, and lays groundwork for intensional, verifiable type theories with richer modal and shape-dependent reasoning.
Abstract
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$, $Φ/\mathsf{extent}$, $Ψ/\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).