论文标题
转付类型：技术报告
The Transpension Type: Technical Report
论文作者
论文摘要
这些注释的目的是给出转发型的分类语义（NUYTS和DEVRIESE，TRANSPENSE：在LMCS，2024年接受的PI-Type的右伴随），这与潜在的子结构依赖性函数类型的伴随。在第2节中，我们讨论了一些先决条件。在第3节中，我们定义乘数并讨论它们的属性。在第4节中，我们研究了乘数如何从基本类别升级为前膜类别。在第5节中，我们解释了如何在the依类型的存在下使用典型的预局部模态。在第6节中，我们研究了先前方式，替代方式和乘数模式的换向特性。
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.
