The Transpension Type: Technical Report
Andreas Nuyts
TL;DR
This work develops a robust categorical semantics for the transpension type, defined as the right adjoint to a potentially substructural dependent function type, by introducing multipliers as base-category endofunctors with weakening functors and lifting them to presheaves. It then constructs four adjoint functors (Σ, Ω, Π, and the transpension) between presheaf categories, investigate their properties, and proves quotient and boundary theorems to manage dimensionally split morphisms and shards. The theory further integrates prior modalities as central or right liftings and establishes comprehensive commutation rules among substitution, modalities, and multipliers, providing a coherent semantic framework for dependent type theories with substructural features. Collectively, these results supply a foundation for modeling transpension within presheaf-based semantic universes and for analyzing interactions with standard presheaf modalities in a dependently typed setting, with potential implications for guarded and fractional type theories.
Abstract
The purpose of these notes is to give a categorical semantics for the transpension type (Nuyts and Devriese, Transpension: The Right Adjoint to the Pi-type, Accepted at LMCS, 2024), which is right adjoint to a potentially substructural dependent function type. In section 2 we discuss some prerequisites. In section 3, we define multipliers and discuss their properties. In section 4, we study how multipliers lift from base categories to presheaf categories. In section 5, we explain how typical presheaf modalities can be used in the presence of the transpension type. In section 6, we study commutation properties of prior modalities, substitution modalities and multiplier modalities.