依赖型理论的代数模型
Algebraic models of dependent type theory
摘要：
史蒂夫·阿沃迪（Steve Awodey）和马塞洛·菲奥雷（Marcelo Fiore）（独立地）观察到，支配具有族的范畴的基本代数概念的规则，精确地匹配了预层之间的可表示自然变换的规则。这为我们提供了一个自然的，函子的描述，基本上是代数对象，用于模型依赖类型理论;以下史蒂夫Awodey，我们称之为“自然模型”。我们可以从几个不同的角度来看待自然模型，在这篇论文中，我们着重讨论了其中的三个。首先，自然模型本质上是代数的，这意味着它们可以通过指定排序之间的操作来描述，服从等式公理;这使我们能够将自然模型组装成具有某些有益性质的类别。第二，由于自然模型是预层之间的自然变换，它们是局部Carnival闭范畴中的态射，这意味着它们可以被视为多项式。第三，由于自然模型承认依赖类型理论的解释，因此我们可以使用它们来提供函式语义。
英文摘要：
The rules governing the essentially algebraic notion of a category with families have been observed (independently) by Steve Awodey and Marcelo Fiore to precisely match those of a representable natural transformation between presheaves. This provides us with a natural, functorial description of essentially algebraic objects which are used to model dependent type theory; following Steve Awodey, we call them 'natural models'. We can view natural models from several different viewpoints, of which we focus on three in this thesis. First, natural models are essentially algebraic, meaning that they can be described by specifying operations between sorts, subject to equational axioms; this allows us to assemble natural models into a category with certain beneficial properties. Second, since natural models are natural transformations between presheaves, they are morphisms in a locally cartesian closed category, meaning that they can be regarded as polynomials. Third, since natural models admit interpretations of dependent type theory, we can use them to provide a functorial semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
