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.

翻译：本笔记旨在为transpension类型（Nuyts和Devriese，《Transpension：Π类型的右伴随》，LMCS 2024录用）提供范畴语义，该类型是潜在子结构依赖函数类型的右伴随。在第2节中，我们讨论了一些预备知识。第3节定义了乘子并讨论其性质。第4节研究乘子如何从基范畴提升到预层范畴。第5节解释在存在transpension类型的情况下如何使用典型预层模态。第6节研究先验模态、替换模态和乘子模态的交换性质。