The Transpension Type: Technical Report

TL;DR

This paper provides a categorical semantics for the transpension type, exploring its properties, how it interacts with modalities, and its lifting from base categories to presheaf categories, advancing the theoretical understanding of this type.

Contribution

It introduces a categorical semantics for the transpension type and analyzes its interaction with various modalities and lifting properties in presheaf categories.

Findings

Defined multipliers and analyzed their properties

Studied how multipliers lift to presheaf categories

Explored the interaction of transpension with presheaf modalities

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.