The twentieth century did not end foundations with one final language. Instead, it produced several powerful ways to organize mathematics: set-theoretic universes, categories, structures, type theories, and homotopical foundations. The lesson is pluralistic: foundations are also tools for seeing connections.
Bourbaki and structures
Bourbaki presented mathematics as a hierarchy of structures: algebraic structures, order structures, topological structures, and their combinations. This style encouraged definitions that travel across fields and made abstraction a working habit.
Definition. A structural viewpoint studies objects through the relations and operations preserved by isomorphism, rather than through the internal material from which the objects are built.
Category theory
Eilenberg and Mac Lane introduced categories to organize natural transformations in algebraic topology. Grothendieck turned categorical language into a vast machine for geometry, cohomology, and schemes.
Proposition. A category records objects and morphisms, and many mathematical constructions are characterized not by elements but by universal properties. Products, quotients, tensor products, and completions often become clearer this way.
Type theory and homotopy
Type theory began as a way to control logical formation rules, later becoming a foundation connected to computation. Homotopy type theory and univalent foundations interpret equality as equivalence-like structure, linking logic, topology, and computer-checked proof.
Principle. In univalent foundations, equivalent structures may be identified in a precise sense. This formalizes a common mathematical habit: isomorphic objects should have the same structural properties.
The nature of modern foundations
Modern foundations are not merely courts of last appeal. They are creative languages. Set theory is excellent for size and hierarchy; category theory for maps and universal properties; type theory for construction and computation; homotopical foundations for spaces of identifications.
Why plurality is not weakness
The nineteenth century sought rigor by reducing ambiguity. The twentieth century learned that different rigorous languages reveal different invariants. A set-theoretic definition may expose hierarchy; a categorical definition may expose functorial behavior; a type-theoretic definition may expose computational content.
This is one of the mature lessons of modern mathematics: foundations do not have to be a single throne. They can be a toolkit of exact languages, each illuminating a different aspect of the same mathematical landscape.
Structures, categories, and type theories
Bourbaki shaped structural style; Eilenberg and Mac Lane created category theory; Grothendieck transformed geometry with categorical methods; Lawvere sought categorical foundations; Martin-Löf developed dependent type theory; Voevodsky advanced univalent foundations and formalized mathematics.
From elements to morphisms
Twentieth-century mathematics increasingly classified an object by how it maps to and from other objects. Eilenberg and Mac Lane introduced categories in the 1940s while organizing algebraic topology. The language made precise a structural habit already visible in Klein's Erlangen program and Emmy Noether's algebra: invariants matter under a specified class of transformations.
Yoneda principle. An object \(A\) in a locally small category is determined up to isomorphism by the functor \[ \operatorname{Hom}(-,A). \] More precisely, \[ \operatorname{Nat}(\operatorname{Hom}(-,A), \operatorname{Hom}(-,B)) \cong\operatorname{Hom}(A,B). \]
This theorem turns the slogan “an object is known by its relationships” into a proof. Universal properties then specify products, tensor products, completions, and free objects without committing to one construction. Different implementations are automatically uniquely isomorphic.
Grothendieck changes the scale of geometry
Grothendieck's schemes replaced algebraic varieties over a field by spaces assembled from spectra of rings. Nilpotents, arithmetic bases, and families became geometric rather than exceptional. Toposes then abstracted the environment in which sheaves and logic live. The shift was characteristic: do not solve each difficult geometric problem in its inherited language; enlarge the language until the operations become natural.
This structural expansion did not erase calculations. It reorganized them. Cohomology packages local-to-global obstructions, derived functors measure the failure of exactness, and representable functors convert moduli questions into geometric objects.
Types, computation, and univalent foundations
Dependent type theory treats propositions as types and proofs as terms. Homotopy type theory interprets equality types as paths and higher equalities as homotopies. Voevodsky's univalence axiom makes equivalence itself a form of identity at the appropriate universe level. This is a foundation designed not only for consistency but for formalized mathematics and machine-checked proof.
No final language, but a growing ecology
Set theory remains the common ambient foundation for most mathematics; category theory supplies a language of structure and transport; type theory connects foundations with computation. Their coexistence is historically instructive. Foundational progress has rarely meant discovering one eternal notation. It has meant learning which language makes a class of invariants, constructions, and proofs visible.