超自然范畴论
摘要：差分范畴中的钢性联性变换与分支定义了一个新的范畴论分支。超自然变换推广了混合变种的二重函子的自然变换，但与其他类似的推广不同，它们是可组合和异常良好的。我们定义了差分函子和超自然变换的范畴，证明了该范畴的一个新的“差分猿耳引理”，并探讨了一些范畴论的含义。 我们还发展了三个引人注目的用途，即参数化多态、难以预测的类型编码和类型理论的差分模型。超自然变换捕捉了参数性的本质，其“超自然条件”与相应的多态类型的“自由定理”完全一致；(共)终结函子关于初始代数、终止余代数、双模和表示独立性提供了一种优雅而通用的框架；“差分猿耳推理”促进了将Grothendieck宇宙提升到差分模型中的类型理论中。我们开发了这些主题并提出了进一步的研究方向。
作者：Jacob Neumann
论文ID：2307.09289
分类：Category Theory
分类简称：math.CT
提交时间：2023-07-19