TY - CHAP
T1 - Univalent Foundations and the Equivalence Principle
AU - Ahrens, Benedikt
AU - North, Paige Randall
PY - 2019
Y1 - 2019
N2 - 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, ‘ 1 ∈ ℕ ’ 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.
AB - 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, ‘ 1 ∈ ℕ ’ 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.
UR - https://www.mendeley.com/catalogue/c82c4fb0-aba5-3b2a-a20a-f4073db0f532/
U2 - 10.1007/978-3-030-15655-8_6
DO - 10.1007/978-3-030-15655-8_6
M3 - Chapter
T3 - Synthese Library
SP - 137
EP - 150
BT - Synthese Library
ER -