论文标题
单价基础和等效原则
Univalent foundations and the equivalence principle
论文作者
论文摘要
在本文中，我们探讨了“等价原理”（EP）：大概，关于数学对象的陈述应在适当的等价概念下不变，而对象类型的对象类型。在集合理论基础中，EP可能并不总是保持：例如，在集合的同构下，语句“ 1 \ in n'并不是不变的。另一方面，在单价基础中，EP已被证明用于许多数学结构。我们首先概述了早期设计满足EP的基础的尝试。然后，我们描述了如何验证EP的基础。
In this paper, we explore the 'equivalence principle' (EP): roughly, statements about mathematical objects should be invariant under an appropriate notion of equivalence for the kinds of objects under consideration. In set theoretic foundations, EP may not always hold: for instance, the statement '1 \in N' is not invariant under isomorphism of sets. In univalent foundations, on the other hand, EP has been proven for many mathematical structures. We first give an overview of earlier attempts at designing foundations that satisfy EP. We then describe how univalent foundations validates EP.
