对称幺半范畴的实用类型理论
摘要：对称单半群范畴的一种自然演绎式类型理论，其判断结构直接表示了带有张量积的态射在其目标对象上以及其源对象上的作用。语法受到了对余代数的Sweedler符号表示的启发，其中变量与域中的类型相关联，而术语与余域中的类型相关联，允许类型在全局上像“元素集合”一样被处理，但受到全局线性类似限制的约束。我们用各种应用程序说明了此类型理论的实用性，例如对偶性、迹、Frobenius单半群和（弱）Hopf单半群。
作者：Michael Shulman
论文ID：1911.00818
分类：Category Theory
分类简称：math.CT
提交时间：2021-07-13