Univalent foundations


Very briefly, the basic idea of the univalence axiom can be explained as follows. In type theoryPlanetmathPlanetmath, one can have a universePlanetmathPlanetmath 𝒰, the terms of which are themselves types, A:𝒰, etc. Those types that are terms of 𝒰 are commonly called small types. Like any type, 𝒰 has an identity type 𝖨𝖽𝒰, which expresses the identity relation A=B between small types. Thinking of types as spaces, 𝒰 is a space, the points of which are spaces; to understand its identity type, we must ask, what is a path p:A↝B between spaces in 𝒰? The univalence axiom says that such paths correspond to homotopy equivalencesMathworldPlanetmathPlanetmath A≃B, (roughly) as explained above. A bit more precisely, given any (small) types A and B, in addition to the primitive type 𝖨𝖽𝒰⁒(A,B) of identifications of A with B, there is the defined type π–€π—Šπ—Žπ—‚π—β’(A,B) of equivalences from A to B. Since the identity map on any object is an equivalence, there is a canonical map,

𝖨𝖽𝒰⁒(A,B)β†’π–€π—Šπ—Žπ—‚π—β’(A,B).

The univalence axiom states that this map is itself an equivalence. At the risk of oversimplifying, we can state this succinctly as follows:

Univalence Axiom:

(A=B)≃(A≃B).

In other words, identityPlanetmathPlanetmathPlanetmathPlanetmath is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to equivalence. In particular, one may say that β€œequivalent types are identical”. However, this phrase is somewhat misleading, since it may sound like a sort of β€œskeletality” condition which collapses the notion of equivalence to coincide with identity, whereas in fact univalence is about expanding the notion of identity so as to coincide with the (unchanged) notion of equivalence.

From the homotopical point of view, univalence implies that spaces of the same homotopy type are connected by a path in the universe 𝒰, in accord with the intuition of a classifying spacePlanetmathPlanetmath for (small) spaces. From the logical point of view, however, it is a radically new idea: it says that isomorphicPlanetmathPlanetmathPlanetmath things can be identified! Mathematicians are of course used to identifying isomorphic structuresMathworldPlanetmath in practice, but they generally do so by β€œabuse of notation”, or some other informal device, knowing that the objects involved are not β€œreally” identical. But in this new foundational scheme, such structures can be formally identified, in the logical sense that every property or construction involving one also applies to the other. Indeed, the identification is now made explicit, and properties and constructions can be systematically transported along it. Moreover, the different ways in which such identifications may be made themselves form a structure that one can (and should!)Β take into account.

Thus in sum, for points A and B of the universe 𝒰 (i.e., small types), the univalence axiom identifies the following three notions:

  • β€’

    (logical) an identification p:A=B of A and B

  • β€’

    (topological) a path p:A↝B from A to B in 𝒰

  • β€’

    (homotopical) an equivalence p:A≃B between A and B.

References

  • 1
Title Univalent foundations
\metatable