• The Univalence Principle Posted by Mike Shulman (guest post by Dimitris Tsementzis, about joint work with Benedikt Ahrens, Paige North, and Mike Shulman) The Univalence Principle is the informal statement that equivalent mathematical structures are indistinguishable. • There are various ways of making this statement formally precise, and a long history of work that does so. • In our recently-published (but long in the making!) book we proved to our knowledge the most general version of this principle, which applies to set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. • This work achieves three main goals. • Firstly, it greatly extends the “Structure Identity Principle” from the original HoTT book, to include any (finite) level of structure, instead of just set-based structures, thus establishing in the strongest sense yet made precise that the Univalent Foundations provide an equivalence-invariant foundation for higher-categorical mathematics. • Secondly, it provides very general novel definitions of equivalence between structures and between objects in a given structure that “compile” to most known notions of equivalence in known cases, but which can also be used to suggest notions in new settings; in doing so it extends M.

Article Summaries:

  • A new book by Shulman, Tsementzis, Ahrens, and North extends the Univalence Principle to a broad class of mathematical structures. The authors prove a general “Structure Identity Principle” that applies to set‑based, categorical, and higher‑categorical objects, not just sets. They introduce novel, highly general definitions of equivalence that recover all familiar notions while suggesting new ones, building on Makkai’s FOLDS framework. The work is carried out in a Two‑Level Type Theory, which provides a metamathematical setting for studying how mathematics is formalized in Univalent Foundations. The result is presented as a foundational metamathematical theorem, strengthening the role of univalence in higher‑category theory.

Sources: