Category Theory (Foundations of Mathematics)

Category theory offers an alternative vision of the foundations of mathematics. Where set theory (ZFC) builds everything out of sets and the membership relation $\in$, category theory takes structure-preserving maps as primitive and describes objects not by what they are made of but by how they relate to everything else — by their universal properties. This "arrows-first" perspective, originating with Eilenberg and Mac Lane and developed into a foundational program by Lawvere and Grothendieck, underlies modern algebraic geometry, topology, type theory, and the homotopy type theory / univalent foundations movement.

This page presents the core notions and then the two foundational programs — elementary topos theory and higher / homotopy type theory — that position category theory as a rival to ZFC. It connects to intuitionistic logic (the internal logic of a topos) and to model theory (categorical logic).

Categories, functors, natural transformations

A category $\mathcal{C}$ consists of:

• a collection of objects $A,B,C,\dots$;
• for each pair of objects a collection of morphisms (arrows) $f:A\to B$, written ${\mathrm{Hom}}_{\mathcal{C}}(A,B)$;
• a composition operation $\circ$ with $g\circ f:A\to C$ for $f:A\to B$, $g:B\to C$;
• an identity morphism ${\mathrm{id}}_A:A\to A$ for each object,

subject to two axioms: associativity $(h\circ g)\circ f=h\circ (g\circ f)$ and identity $f\circ {\mathrm{id}}_A=f={\mathrm{id}}_B\circ f$. Note the objects are almost incidental — a category is essentially a world of arrows that compose. Examples: $\mathbf{Set}$ (sets and functions), $\mathbf{Grp}$ (groups and homomorphisms), $\mathbf{Top}$ (spaces and continuous maps), a poset (one arrow $a\to b$ iff $a\le b$), a monoid (one object, elements as arrows).

The key move is that the same structural notions recur across all these categories:

• A functor $F:\mathcal{C}\to \mathcal{D}$ maps objects to objects and arrows to arrows, preserving composition and identities — a "homomorphism of categories." Functors are how constructions (free group, fundamental group ${\pi }_1$, power set) are made precise as operations on whole categories.
• A natural transformation $\eta :F\Rightarrow G$ is a family of morphisms ${\eta }_A:F(A)\to G(A)$ commuting with all arrows — a "morphism of functors." Eilenberg and Mac Lane introduced categories and functors in order to define natural transformations; "natural" got a precise meaning at last.

Functors and natural transformations themselves form a functor category $[\mathcal{C},\mathcal{D}]$, and the whole apparatus is famously self-referential — categories of categories, $\mathbf{Cat}$.

Universal properties and the Yoneda lemma

The signature of categorical thinking is the universal property: defining an object by a mapping-in or mapping-out condition that determines it uniquely up to unique isomorphism. Examples:

• Products $A\times B$, coproducts $A+B$; the terminal object $1$ and initial object $0$;
• Limits and colimits (pullbacks, equalizers, inverse/direct limits) — general "best approximations" to a diagram;
• Exponentials $B^A$ (function objects) in a cartesian closed category — the categorical home of the typed $\lambda$-calculus and intuitionistic logic.

The Yoneda lemma — the deepest elementary fact in the subject — says an object is completely determined by the network of morphisms into (or out of) it:

$$\mathrm{Nat}(\mathrm{Hom}(A,-),F)\cong F(A),$$

and in particular $A\mapsto \mathrm{Hom}(A,-)$ embeds $\mathcal{C}$ fully and faithfully into a functor category. Philosophically: to know an object is to know how everything maps to it. This is the precise sense in which category theory is "relational" rather than "elemental."

Adjunctions and monads

An adjunction $F⊣G$ between functors $F:\mathcal{C}\to \mathcal{D}$ and $G:\mathcal{D}\to \mathcal{C}$ is a natural bijection

$${\mathrm{Hom}}_{\mathcal{D}}(FA,B)\cong {\mathrm{Hom}}_{\mathcal{C}}(A,GB).$$

Adjunctions are ubiquitous — free–forgetful pairs (free group ⊣ underlying set), product–exponential ($-\times A⊣(-{)}^A$), and existential/universal quantifiers as adjoints to substitution (Lawvere's hyperdoctrines, linking to first-order logic). "Adjoint functors arise everywhere" (Mac Lane). An adjunction induces a monad $T=GF$ on $\mathcal{C}$, an algebraic gadget axiomatizing "a notion of structure" (and, in computer science, "a notion of computation/effect").

Categorical foundations I — elementary topos theory

Lawvere and Tierney's elementary topos is a category abstracting the essential features of $\mathbf{Set}$ well enough to serve as a universe of sets. A topos is a cartesian closed category with all finite limits and a subobject classifier $\Omega$ — an object of "truth values" with a universal monomorphism $\mathrm{true}:1\to \Omega$ such that subobjects of any $A$ correspond to maps $A\to \Omega$. The subobject classifier internalizes logic:

• In $\mathbf{Set}$, $\Omega =\{0,1\}$ and the theory is classical.
• In a general topos, $\Omega$ is a Heyting algebra, so the internal logic of a topos is intuitionistic, not classical. Excluded middle and Choice need not hold.

Two foundational payoffs:

• ETCS (Lawvere's Elementary Theory of the Category of Sets) axiomatizes $\mathbf{Set}$ itself categorically — a foundation equivalent in strength to a slightly weakened ZFC (bounded Zermelo with Choice), formulated entirely in terms of functions and composition, with no global $\in$ relation. Membership becomes a local, derived notion.
• Sheaf and presheaf topoi $[{\mathcal{C}}^{\mathrm{op}},\mathbf{Set}]$ provide models in which independence results become geometry: Cohen forcing for the independence of CH is, in this light, a construction of a topos (a Boolean-valued / sheaf model). Topos theory thus reinterprets set-theoretic independence categorically.

Grothendieck topoi additionally power modern algebraic geometry (sites, étale cohomology), and the internal language of a topos lets one reason about its objects "as if" they were sets, in intuitionistic higher-order logic.

Categorical foundations II — type theory and univalence

The second foundational program connects categories to constructive type theory via the Curry–Howard correspondence, extended to a three-way Curry–Howard–Lambek correspondence:

$$\text{intuitionistic logic}\leftrightarrow \text{typed }\lambda \text{-calculus}\leftrightarrow \text{cartesian closed categories}.$$

Propositions are types are objects; proofs are programs are morphisms. Dependent type theory corresponds to locally cartesian closed categories and fibrations.

The modern culmination is Homotopy Type Theory (HoTT) / Univalent Foundations (Voevodsky and others):

• types are interpreted as spaces (∞-groupoids / objects of an $(\infty ,1)$-category), terms as points, and the identity type ${\mathrm{Id}}_A(x,y)$ as the path space — equality is a structure (a path), not a mere proposition;
• Voevodsky's univalence axiom asserts that equality of types is equivalence of types ($\mathrm{Id}(A,B)\simeq (A\simeq B)$), formalizing the everyday mathematical practice of "identifying isomorphic structures";
• higher inductive types build spaces (circles, spheres, quotients) directly, making synthetic homotopy theory possible inside the foundation.

HoTT is a foundation in which "sets" are merely the $0$-truncated types at the bottom of a tower of higher groupoids — a genuinely different starting point from ZFC, and one designed for machine-checked mathematics (it is the basis of substantial libraries in Coq/Rocq, Agda, and Lean).

Set theory vs. category theory as foundations

The two are not strictly rivals so much as complementary lenses: ETCS and bounded ZFC are intertranslatable, and most working mathematics is indifferent to which is "underneath." But the structural stance — objects up to isomorphism, defined by universal properties, with an intuitionistic internal logic — is increasingly the native language of geometry, topology, and computer-checked proof.

Summary

• A category is objects + composable arrows; functors map between categories and natural transformations between functors.
• Universal properties (limits, colimits, exponentials, adjunctions) define objects by their relationships; the Yoneda lemma says an object is its web of morphisms.
• Topos theory (ETCS, elementary/sheaf topoi) gives a structural foundation whose internal logic is intuitionistic and which recasts set-theoretic independence as geometry.
• Type-theoretic foundations (Curry–Howard–Lambek, HoTT/univalence) identify logic, computation, and category theory, supplying the basis for modern mechanized mathematics.

Category theory reframes the foundations of mathematics around structure and transformation rather than membership and element, offering — through topos theory and homotopy type theory — genuine alternatives to ZFC that are intuitionistic by nature and especially suited to geometry and formalized proof.