类型论（三）
7。单价基础
类型理论，集合理论和类别理论之间的联系通过对单价基础（Voevodsky 2015）和单位公理的工作获得了新的启示。这涉及到上一节中描述的类型理论的扩展，特别是类型的类型，命题视图作为类型的观点以及类型宇宙的概念。这些发展也与讨论结构的概念有关，例如，在罗素1959年强调了结构的重要性。
Martin-Löf1975 [1973]引入了新的基本类型IDA（A，B），如果A和B在A型中，可以将其视为元素A和B的平等证明类型。这种新类型的一个重要特征是它可以迭代，因此，如果P和Q是IDA类型（A，B），则可以考虑IDIDA类型（A，B）（P，Q）。如果我们认为一种类型是一种特殊的集合，那么自然而然地认为，这种平等证明总是容纳任何两个平等证明P和Q。确实，直觉上，两个要素A和B之间似乎最多可以证明平等的证明。令人惊讶的是，Hofmann and Streicher 1996设计了一个依赖类型理论的模型，在该模型中这是无效的，这是一个模型，它们可以是两个元素相等的不同证据。在此模型中，类型是由groupoid和类型IDA（a，b）解释的A和B之间的同构，该集合可能具有多个元素。该模型的存在的结果是，在类型理论中，不能证明平等类型最多具有一个元素。该类别解释已通过以下方式推广，从而提供了对身份类型的直观解释。一种类型由拓扑空间解释，直至同型，而IDA类型（a，b）通过连接A和B的路径的类型来解释。 （请参阅Awodey等人，2013年和[Hott 2013，其他互联网资源]。
Voevodsky 2015引入了以下类型分层。 （这种分层的一部分是由于这种类型作为拓扑空间的解释而动机，但可以直接理解而无需参考这种解释。）我们说，如果我们有任何IDA（a，b），则A类型是一种命题A的元素A和B（这意味着A类型最多具有一个元素）。我们说，如果IDA类型（a，b）是A的任何元素a和b的命题。设置为A的任何元素A和B的元素A和B的理由是，只能使用类型理论规则显示，任何此类类型确实可以被视为通常的分类意义上的群体素是这个元素类型，A和B之间的形态集由IDA（a，b）表示。组成是平等传递性的证明，身份形态是平等反射性的证明。每个形态都有逆的事实对应于身份是对称关系的事实。然后可以扩展该分层，我们可以定义何时类型为2组，3组等。在这种观点中，类型理论似乎是集合理论的广泛概括，因为一组是一种特殊的类型。
Voevodsky 2015还引入了类型之间的等效性概念，以统一的方式概括了命题之间的逻辑等效性，两组之间的逻辑等价概念，集合之间的培训，群体固体之间的分类等效性等等。我们说，如果b中的任何元素b，p的类型p，p是IDB类型（fa，b），则映射f：a→b是一个等效性。这以强烈的方式表达了B中的元素是A中的一个元素的图像，如果设置A和B，我们恢复了集合之间的两者的常规概念。 （通常，如果f：a→b是等价性，那么我们有一个映射b→a，可以将其视为f的倒数）。令Equiv（a，b）为对f，p，其中f：a→b和p是f是等效性的证明。利用身份图是一个等效性的事实，我们对任何类型A的equiv（a，a）元素。这意味着我们有一个映射
idu（a，b）→epiv（a，b）
单相关的公理表明，该图是一个等效性。特别是我们有含义
equiv（a，b）→idu（a，b）
因此，如果两种小型类型之间存在等效性，那么这些类型相等。
该公理可以看作是扩展性原理的强大形式。它确实概括了教会1940年提到的命题扩展的公理，该命题扩展性在逻辑上等同于同等。令人惊讶的是，这也意味着功能扩展的公理，1940年教堂中的公理10，它指出了两个点相等的功能是相等的（Voevodsky 2015）。这也直接暗示两个同构集相等，两个绝对等效的类固醇相等，所以一个是相等的。
这可以用来列出结构运输概念（Bourbaki 1957）。例如，让MA为集合A上的单体结构的类型单律定律。平等替换的规则以平等为
idu（a，b）→ma→mb
如果A和B之间有两次两者的两次两次射击，则它们与单位的公理相等，我们可以使用这种含义来运输B中A中A的任何单体结构。
罗素（Russell）1919年和1959年的罗素（Russell）都强调了结构概念的重要性。例如，在罗素（Russell）1919章的第六章中，注意到两个类似的关系基本上具有相同的属性，因此具有相同的“结构”。 （Russell 1901中引入了关系的“相似性”概念。）我们还可以使用该框架来完善罗素关于结构概念的讨论。例如，让monoid为对a，p的类型，其中p是ma的元素。如果存在从a到b的两次循环f，则两个这样的对A，P和B，Q是同构的，使得Q等于P沿F的结构的运输。单位公理的结果是，类型类型的两个同构元相等，因此具有相同的特性。请注意，当在集合理论框架中制定结构时，不可能进行这种性能的一般运输。实际上，在集合理论框架中，可以使用成员关系来制定属性，例如结构的载体集包含自然数0的属性，该属性属性通常不保留在同构中。从直觉上讲，结构的集合理论描述还不够抽象，因为我们可以谈论这种结构的构建方式。集合理论和类型理论之间的这种差异是J.Reynolds 1983将类型结构作为“实施抽象水平的句法学科”的表征的另一个例证。
