依赖类型理论的代数模型
摘要：范畴与家族概念的基本代数规则被Steve Awodey和Marcelo Fiore（独立地）观察到，与预设集之间的可表示自然变换的规则完全匹配。这为我们提供了自然的、函子化的描述方式，用于模拟依赖类型理论的基本代数对象；我们称之为“自然模型”，跟随Steve Awodey的称呼。 我们可以从几个不同的视角看待自然模型，本文将重点讨论其中的三个。首先，自然模型本质上是代数的，这意味着它们可以通过指定不同类型之间的操作并遵循等式公理来描述；这使我们能够将自然模型组合成具有特定有益属性的范畴。其次，由于自然模型是预设集之间的自然变换，它们可以被看作是局部笛卡尔闭范畴中的态射，也就是多项式。第三，由于自然模型可以解释依赖类型理论，我们可以利用它们提供的函子语义。
作者：Clive Newstead
论文ID：2103.06155
分类：Category Theory
分类简称：math.CT
提交时间：2021-03-11