Title: The Structure Identity Principle in Set Theory and Type Theory.
Abstract: The Structure Identity Principle (SIP) states that
Isomorphic structures are structurally identical. After discussing
SIP in the setting of set-theoretical mathematical practice and
formulating a precise general notion of mathematical structure I will
prove a theorem of Homotopy Type Theory. The theorem states that a
strong form of SIP for that notion of mathematical structure, as
represented in intensional dependent type theory, is a consequence of
a new axiom for type theory, Voevodsky's Univalence Axiom. The strong
form of SIP expresses that isomorphic structures are identical.