Higher categories · The Lumenary

MotivationH

Why go up a dimension?

A category records objects and arrows, and asks whether two arrows are equal. Again and again, mathematics hands us arrows that are not equal but are related in a structured way:

Two functors $F, G : \mathcal{C} \to \mathcal{D}$ are compared by natural transformations $F \Rightarrow G$ — arrows between arrows. Categories, functors and natural transformations form something with three layers.
In a monoidal category such as vector spaces under $\otimes$ , the objects $(U \otimes V) \otimes W$ and $U \otimes (V \otimes W)$ are not equal but canonically isomorphic, and the isomorphisms satisfy laws of their own (Mac Lane's pentagon).
Rings $R, S$ and $(R, S)$ -bimodules compose by tensor product, ${}_R M_S \otimes_S {}_S N_T$ , which is associative only up to isomorphism; bimodule maps are arrows between these arrows. (This is the Morita bicategory.)
In a space $X$ , paths compose only up to homotopy; homotopies between paths are arrows between arrows, and homotopies between homotopies go one level higher. The fundamental groupoid of the fundamental-group lesson forgets all of this higher information.

Higher category theory is the study of structures with $k$ -morphisms between $(k-1)$ -morphisms for $k = 1, 2, \dots, n$ (or for all $k$ ). Dimension 2 is completely understood and is the main subject of this lesson; dimension 3 is understood, with a surprise; beyond that the subject branches into several competing definitions, and the $(\infty, 1)$ case has its own lesson, ∞-categories.

IntuitionH

Cells, pasting and the two compositions

Picture a 2-category as a world of cells: 0-cells (objects) are points, 1-cells are arrows between points, and 2-cells are surfaces between parallel arrows.

Globular picture of 2-cells. Vertically, α : F ⇒ G and β : G ⇒ H stack to give β·α : F ⇒ H. Horizontally, α and γ : I ⇒ J sit side by side to give γ∗α : IF ⇒ JG. The interchange law says the whole picture has one meaning, however it is cut up.

Two 2-cells can be composed in two directions: vertically (along a shared 1-cell) and horizontally (along a shared 0-cell). The picture above can be evaluated "rows first" — compose $\alpha, \beta$ and $\gamma, \delta$ vertically, then horizontally — or "columns first". The interchange law says the answers agree:

(\delta \cdot \gamma) \ast (\beta \cdot \alpha) = (\delta \ast \beta) \cdot (\gamma \ast \alpha).

The second idea is weakness. In $\mathbf{Cat}$ , composition of functors is associative on the nose. In the Morita bicategory it is not: $(M \otimes N) \otimes P$ and $M \otimes (N \otimes P)$ are different modules, related by a canonical isomorphism. A bicategory keeps these isomorphisms as part of the data and imposes laws on them. Going up a dimension means that equations between 1-cells may be replaced by invertible 2-cells — and then those 2-cells must satisfy equations of their own.

DefinitionsH

2-categories, bicategories and pseudofunctors

Throughout, juxtaposition $gf$ means $g \circ f$ ("first $f$ , then $g$ "); Lean and Mathlib write the same composite in diagrammatic order as f ≫ g.

Definition— strict 2-category

A strict 2-category $\mathcal{K}$ consists of

a collection of objects (0-cells) $a, b, c, \dots$ ;
for each pair of objects a category $\mathcal{K}(a, b)$ , whose objects $f : a \to b$ are the 1-cells and whose morphisms $\alpha : f \Rightarrow g$ are the 2-cells; composition in $\mathcal{K}(a, b)$ is vertical composition $\beta \cdot \alpha$ ;
for each triple of objects a functor $\circ : \mathcal{K}(b, c) \times \mathcal{K}(a, b) \to \mathcal{K}(a, c)$ , written $(g, f) \mapsto gf$ on 1-cells and $(\gamma, \alpha) \mapsto \gamma \ast \alpha$ on 2-cells (horizontal composition);
an identity 1-cell $1_a$ for each object,

such that horizontal composition is strictly associative and unital: $(hg)f = h(gf)$ , $f 1_a = f = 1_b f$ , and likewise for 2-cells. That $\circ$ is a functor on the product category says exactly that $1_g \ast 1_f = 1_{gf}$ and that the interchange law holds.

Definition— bicategory

A bicategory $\mathcal{B}$ (Bénabou, 1967) has the same data as a 2-category, except that horizontal composition is associative and unital only up to coherent invertible 2-cells: there are natural isomorphisms

\alpha_{h,g,f} : (hg)f \Rightarrow h(gf), \qquad \lambda_f : 1_b f \Rightarrow f, \qquad \rho_f : f 1_a \Rightarrow f

(the associator and unitors), natural in $f, g, h$ , satisfying two axioms. For composable $f : a \to b$ , $g : b \to c$ , $h : c \to d$ , $k : d \to e$ :

pentagon: $(1_k \ast \alpha_{h,g,f}) \cdot \alpha_{k, hg, f} \cdot (\alpha_{k,h,g} \ast 1_f) = \alpha_{k,h,gf} \cdot \alpha_{kh,g,f}$ as 2-cells $((kh)g)f \Rightarrow k(h(gf))$ ;
triangle: $(1_g \ast \lambda_f) \cdot \alpha_{g, 1_b, f} = \rho_g \ast 1_f$ as 2-cells $(g 1_b) f \Rightarrow g f$ .

A strict 2-category is a bicategory whose associators and unitors are identities.

Definition— pseudofunctor

A pseudofunctor $F : \mathcal{B} \to \mathcal{B}'$ sends objects, 1-cells and 2-cells to objects, 1-cells and 2-cells, is a functor on each hom-category, and preserves composition and identities only up to coherent invertible 2-cells $F(g) F(f) \Rightarrow F(gf)$ and $1_{Fa} \Rightarrow F(1_a)$ , subject to compatibility with the associators and unitors. It is a 2-functor when these 2-cells are identities. A biequivalence is a pseudofunctor that is essentially surjective on objects up to equivalence and an equivalence on every hom-category.

Definition— monoidal category

A monoidal category (see Monoidal categories) is a category $\mathcal{C}$ with a functor $\otimes : \mathcal{C} \times \mathcal{C} \to \mathcal{C}$ , a unit object $I$ and natural isomorphisms $(X \otimes Y) \otimes Z \cong X \otimes (Y \otimes Z)$ , $I \otimes X \cong X$ , $X \otimes I \cong X$ satisfying the pentagon and triangle axioms.

Worked examplesH

Examples and non-examples

Example— The strict 2-category Cat

Objects are (small) categories, 1-cells are functors, 2-cells are natural transformations. Vertical composition is componentwise: $(\beta \cdot \alpha)_X = \beta_X \circ \alpha_X$ . For $\alpha : F \Rightarrow G$ between functors $\mathcal{C} \to \mathcal{D}$ and $\gamma : I \Rightarrow J$ between functors $\mathcal{D} \to \mathcal{E}$ , the horizontal composite $\gamma \ast \alpha : IF \Rightarrow JG$ has components

(\gamma \ast \alpha)_X = J(\alpha_X) \circ \gamma_{FX} = \gamma_{GX} \circ I(\alpha_X),

the two expressions agreeing by naturality of $\gamma$ at $\alpha_X$ . Composition of functors is associative and unital on the nose, so $\mathbf{Cat}$ is strict.

Example— One-object bicategories are monoidal categories

If $\mathcal{B}$ has a single object $\star$ , the hom-category $\mathcal{C} = \mathcal{B}(\star, \star)$ carries a tensor product $g \otimes f := gf$ (horizontal composition), unit $I := 1_\star$ , and the associator and unitors of $\mathcal{B}$ ; the pentagon and triangle are word for word the monoidal axioms. Conversely, a monoidal category $(\mathcal{C}, \otimes, I)$ gives a bicategory $\Sigma\mathcal{C}$ with one object, 1-cells the objects of $\mathcal{C}$ , 2-cells the morphisms of $\mathcal{C}$ , and composition $\otimes$ . So a monoidal category is a bicategory with one object — "delooping" shifts everything down one dimension. Mathlib has both directions (see the formal section).

Example— Spans, bimodules and the fundamental 2-groupoid

Spans. In a category with pullbacks, a 1-cell $a \to b$ is a span $a \leftarrow s \rightarrow b$ , composition is by pullback and 2-cells are maps of spans. Pullbacks are defined only up to unique isomorphism, so composition is associative only up to isomorphism: a genuine bicategory (Bénabou's original example).
Bimodules. Objects are rings, 1-cells $R \to S$ are $(S, R)$ -bimodules, composition is $\otimes$ and 2-cells are bimodule maps. Two rings are equivalent in this bicategory exactly when they are Morita equivalent.
The fundamental 2-groupoid $\Pi_2(X)$ of a space: points, paths, and homotopy classes (rel endpoints) of homotopies between paths. Concatenation of paths is associative only up to reparametrisation homotopy, so $\Pi_2(X)$ is a bicategory in which every 2-cell is invertible and every 1-cell is invertible up to a 2-cell (a bigroupoid).

Example— A non-example, and a surprise

Take a "2-category with one object $\star$ and one 1-cell $1_\star$ ". Its 2-cells form a set with two operations, vertical and horizontal composition, both unital with unit $1_{1_\star}$ and linked by interchange. By the Eckmann–Hilton argument below, the two operations coincide and are commutative. So you cannot model a non-commutative group as the 2-cells of a doubly degenerate 2-category: a monoid becomes forced to be commutative when it is pushed up two dimensions. This is the categorical shadow of the fact that $\pi_2(X)$ is abelian.

ProofH

Central theorems

Theorem— Theorem 1 (the interchange law in Cat)

Let $\alpha : F \Rightarrow G$ , $\beta : G \Rightarrow H$ be natural transformations between functors $\mathcal{C} \to \mathcal{D}$ , and $\gamma : I \Rightarrow J$ , $\delta : J \Rightarrow K$ between functors $\mathcal{D} \to \mathcal{E}$ . Then

(\delta \cdot \gamma) \ast (\beta \cdot \alpha) = (\delta \ast \beta) \cdot (\gamma \ast \alpha).

Proof

Both sides are natural transformations $IF \Rightarrow KH$ ; compare components at an object $X$ of $\mathcal{C}$ , using $(\gamma \ast \alpha)_X = J(\alpha_X) \circ \gamma_{FX}$ . The left side is

K\big((\beta \cdot \alpha)_X\big) \circ (\delta \cdot \gamma)_{FX} = K(\beta_X) \circ K(\alpha_X) \circ \delta_{FX} \circ \gamma_{FX}.

The right side is

(\delta \ast \beta)_X \circ (\gamma \ast \alpha)_X = K(\beta_X) \circ \delta_{GX} \circ J(\alpha_X) \circ \gamma_{FX}.

Naturality of $\delta$ at the morphism $\alpha_X : FX \to GX$ says $\delta_{GX} \circ J(\alpha_X) = K(\alpha_X) \circ \delta_{FX}$ . Substituting this into the right side gives the left side.

∎

The same computation shows that horizontal composition is associative and unital, so $\mathbf{Cat}$ is a strict 2-category.

Theorem— Theorem 2 (Eckmann–Hilton, 1962)

Let $X$ be a set with binary operations $\odot$ and $\star$ , with two-sided units $e_\odot$ and $e_\star$ , satisfying the interchange law

(a \star b) \odot (c \star d) = (a \odot c) \star (b \odot d) \qquad \text{for all } a, b, c, d \in X.

Then $e_\odot = e_\star$ , the operations coincide, and the common operation is commutative (and associative).

Proof

Units. Put $a = d = e_\star$ and $b = c = e_\odot$ : $e_\odot = e_\odot \odot e_\odot = (e_\star \star e_\odot) \odot (e_\odot \star e_\star) = (e_\star \odot e_\odot) \star (e_\odot \odot e_\star) = e_\star \star e_\star = e_\star.$ Call the common unit $e$ .

The operations agree. For all $a, b$ : $a \odot b = (a \star e) \odot (e \star b) = (a \odot e) \star (e \odot b) = a \star b.$

Commutativity. For all $a, b$ : $a \star b = a \odot b = (e \star a) \odot (b \star e) = (e \odot b) \star (a \odot e) = b \star a.$

Associativity. $(a \star b) \star c = (a \star b) \odot (e \star c) = (a \odot e) \star (b \odot c) = a \star (b \star c)$ .

∎

The Eckmann–Hilton argument as a picture (2-cells point downwards, so η above θ is the vertical composite θ·η). Using units, the two cells shrink and slide around each other in the plane until θ sits above η, which is η·θ. In one dimension there is no room to pass, which is why ordinary monoids need not be commutative.

Theorem— Corollary 3 (2-endomorphisms of identities commute)

In any bicategory $\mathcal{B}$ , for any object $a$ and any 2-cells $\eta, \theta : 1_a \Rightarrow 1_a$ , we have $\eta \cdot \theta = \theta \cdot \eta$ . In particular, natural transformations $1_{\mathcal{C}} \Rightarrow 1_{\mathcal{C}}$ of the identity functor commute, and in a monoidal category the endomorphisms of the unit object $I$ commute.

Proof

The interchange law for the two whiskerings of $\eta$ and $\theta$ says $(\eta \ast 1_{1_a}) \cdot (1_{1_a} \ast \theta) = (1_{1_a} \ast \theta) \cdot (\eta \ast 1_{1_a})$ , as 2-cells $1_a 1_a \Rightarrow 1_a 1_a$ (both sides equal $\eta \ast \theta$ ). Whiskering by an identity is conjugation by a unitor: by naturality of $\lambda$ and $\rho$ ,

1_{1_a} \ast \theta = \lambda^{-1}_{1_a} \cdot \theta \cdot \lambda_{1_a}, \qquad \eta \ast 1_{1_a} = \rho^{-1}_{1_a} \cdot \eta \cdot \rho_{1_a}.

A standard consequence of the pentagon and triangle axioms is $\lambda_{1_a} = \rho_{1_a}$ (Kelly, 1964, for monoidal categories). Writing $u$ for this isomorphism, the interchange equation becomes $u^{-1} \cdot \eta \cdot \theta \cdot u = u^{-1} \cdot \theta \cdot \eta \cdot u$ , and cancelling the isomorphism $u$ gives $\eta \cdot \theta = \theta \cdot \eta$ . (Equivalently: the set of such 2-cells carries vertical composition and a second unital operation $\eta \star \theta := u \cdot (\eta \ast \theta) \cdot u^{-1}$ satisfying interchange; apply Theorem 2.)

∎

The same argument, in $\Pi_2(X, x)$ or with maps of squares $[0,1]^2 \to X$ , proves that $\pi_2(X, x)$ — and every $\pi_n$ with $n \ge 2$ — is abelian.

Theorem— Theorem 4 (coherence for bicategories; stated, not proved here)

Every bicategory is biequivalent to a strict 2-category. Moreover, in a bicategory all diagrams built from associators and unitors (formal composites, between the same two bracketings) commute.

The first statement is due to Mac Lane and Paré (1985), and can also be deduced from a bicategorical Yoneda lemma: embed $\mathcal{B}$ into the strict 2-category of pseudofunctors $\mathcal{B}^{\mathrm{op}} \to \mathbf{Cat}$ (Street). A careful modern treatment, via the bicategorical Yoneda lemma, is in Johnson and Yau, 2-Dimensional Categories. For one-object bicategories this reduces to coherence for monoidal categories (Mac Lane, 1963; see also Joyal and Street): all diagrams of associators and unitors commute, and every monoidal category is monoidally equivalent to a strict one. The practical meaning is that one may calculate in a bicategory as if it were strict — provided one remembers that the strictification changes the objects.

Theorem— Theorem 5 (Gordon–Power–Street, 1995; stated, not proved here)

Every tricategory is triequivalent to a Gray-category — a semi-strict 3-category in which everything is strict except the interchange law, which holds only up to a coherent invertible 3-cell. It is not true that every tricategory is triequivalent to a strict 3-category.

The failure of full strictification is visible in homotopy theory. Simpson (1998) showed that the homotopy 3-type of the 2-sphere $S^2$ cannot be modelled by a strict 3-groupoid. Roughly, a strict interchange law forces the invariant linking $\pi_2$ and $\pi_3$ of a simply connected strict 3-groupoid to vanish (the braiding obtained by sliding one 2-cell around another becomes trivial), whereas for $S^2$ this invariant is non-zero: it is detected by the Hopf map, which generates $\pi_3(S^2) \cong \Z$ . Strictification works in dimension 2 and fails from dimension 3 on; the "weak interchange" of Gray-categories is exactly the missing ingredient.

ExplanationH

The landscape: what is known and what is open

Established.

Dimension 2. Bicategories, pseudofunctors, pseudonatural transformations and modifications form a well-understood theory, with coherence (Theorem 4), a Yoneda lemma, adjunctions and monads (Johnson–Yau 2021; Lack's 2-categories companion, 2010).
Dimension 3. Tricategories were defined by Gordon, Power and Street (1995); coherence holds in the Gray-category form (Theorem 5; see Gurski, Coherence in Three-Dimensional Category Theory, 2013).
Degenerate cases and the periodic table. A bicategory with one object is a monoidal category; a tricategory with one object and one 1-cell is (essentially) a braided monoidal category; one more level of degeneracy gives symmetric monoidal structure, after which nothing new appears. This pattern is the periodic table of Baez and Dolan (1995). Making "is the same as" precise is subtle: Cheng and Gurski (2007) showed that the comparison works on objects but must be stated carefully once morphisms and higher morphisms are compared. A version of the Baez–Dolan stabilization hypothesis has been proved in the $(\infty, n)$ -categorical setting (Gepner and Haugseng, 2015).
$(\infty, 1)$ -categories. When all $k$ -morphisms with $k \ge 2$ are invertible, there are several equivalent, fully developed models (quasi-categories, complete Segal spaces, simplicial categories) — the subject of the next lesson.

Several definitions of weak $n$ -category. For general $n$ there is no single accepted definition. Leinster's survey (2002) lists ten, including: Batanin's and Leinster's (globular operads), Trimble's, Street's (simplicial, via "orientals" and complicial sets, later developed by Verity), Tamsamani's and Simpson's (Segal-type, iterated simplicial), Baez and Dolan's (opetopic), Joyal's ( $\Theta$ -categories) and Rezk's ( $\Theta_n$ -spaces, for $(\infty, n)$ -categories).

Open or in progress. Comparing these definitions is research. Some comparisons are proved (for instance among several models of $(\infty, n)$ -categories, and an axiomatic characterisation of the homotopy theory of $(\infty, n)$ -categories by Barwick and Schommer-Pries, published 2021), but a complete comparison of all proposed definitions of weak $n$ -category is not available. Fully explicit algebraic definitions with coherence theorems exist for $n \le 3$ ; Trimble wrote down an explicit definition of tetracategories ( $n = 4$ ), and explicit definitions become unmanageable by hand beyond that — one reason the field moved towards homotopical (" $\infty$ ") models.

Formal mathematicsF

Higher categories in Lean and Mathlib

Mathlib has a substantial library for dimension 2: bicategories (CategoryTheory.Bicategory, with associators, unitors, the pentagon and the triangle as axioms), strict bicategories, pseudofunctors, the strict 2-category Cat, the monoidal category of endomorphisms of an object, and the one-object bicategory of a monoidal category. Note the conventions: Mathlib composes 1-cells and morphisms in diagrammatic order (f ≫ g is "first f, then g") and writes horizontal composition of natural transformations as α ◫ γ, with components (α ◫ γ).app X = γ.app (F.obj X) ≫ J.map (α.app X) — the formula $J(\alpha_X) \circ \gamma_{FX}$ of the examples section.

The interchange law, proved from naturality exactly as in Theorem 1 (after ext X and unfolding, one use of the naturality of δ finishes the proof), and Mathlib's own version:

interchangeLean 4Proved here from basic factsFormally verified

/-- **The interchange law** in the 2-category of categories. For natural transformations
`α : F ⟶ G`, `β : G ⟶ H` (between functors `C ⥤ D`) and `γ : I ⟶ J`, `δ : J ⟶ K` (between
functors `D ⥤ E`), composing vertically first and then horizontally (`◫`) gives the same
result as composing horizontally first and then vertically:
`(α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ)`.
Mathlib's horizontal composite has components `(α ◫ γ)_X = γ_{F X} ≫ J(α_X)`. At an object `X`
the two sides differ only by the order of `δ_{F X}` and `J(α_X)`, and the naturality square
of `δ` at the morphism `α_X` swaps them. -/
theorem interchange {C D E : Type*} [Category C] [Category D] [Category E]
    {F G H : C ⥤ D} {I J K : D ⥤ E}
    (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) :
    (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ) := by
  ext X
  simp only [NatTrans.hcomp_app, NatTrans.comp_app, Functor.map_comp, Category.assoc]
  -- Goal: γ ≫ δ_{FX} ≫ K(α_X) ≫ K(β_X) = γ ≫ J(α_X) ≫ δ_{GX} ≫ K(β_X) (γ at F X).
  -- Naturality of `δ` at `α_X : F X ⟶ G X`: `J(α_X) ≫ δ_{GX} = δ_{FX} ≫ K(α_X)`.
  rw [δ.naturality_assoc]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

interchange_libraryLean 4Applies a library theoremFormally verified

/-- The interchange law again, now by Mathlib's `CategoryTheory.NatTrans.exchange`
(proved there by the automation `cat_disch`, which finds the same naturality argument). -/
theorem interchange_library {C D E : Type*} [Category C] [Category D] [Category E]
    {F G H : C ⥤ D} {I J K : D ⥤ E}
    (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) :
    (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ) :=
  NatTrans.exchange α β γ δ

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

cat_strictLean 4Applies a library theoremFormally verified

/-- Categories, functors and natural transformations form a **strict** 2-category: composition
of functors is associative and unital on the nose, so Mathlib's bicategory structure on `Cat`
has associators and unitors that are identities (`eqToIso` of equalities). This is Mathlib's
instance `CategoryTheory.Cat.bicategory.strict`. -/
theorem cat_strict : Bicategory.Strict Cat.{0, 0} :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

The Eckmann–Hilton argument, with a calc proof that follows Theorem 2 line by line (the units first, then agreement, then commutativity), and Mathlib's version, which it uses to prove that higher homotopy groups are abelian:

units_coincideLean 4Proved here from basic factsFormally verified

/-- If two binary operations each have a two-sided unit (`e₁` for `m₁`, `e₂` for `m₂`) and
satisfy the interchange law `m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)`, then the units are
equal. Proof: put `a = d = e₂` and `b = c = e₁` in the interchange law; the left side
collapses to `m₁ e₁ e₁ = e₁` and the right side to `m₂ e₂ e₂ = e₂`. -/
theorem units_coincide {X : Type*} (m₁ m₂ : X → X → X) (e₁ e₂ : X)
    (h₁l : ∀ a, m₁ e₁ a = a) (h₁r : ∀ a, m₁ a e₁ = a)
    (h₂l : ∀ a, m₂ e₂ a = a) (h₂r : ∀ a, m₂ a e₂ = a)
    (interchange : ∀ a b c d, m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
    e₁ = e₂ :=
  calc e₁ = m₁ e₁ e₁ := (h₁l e₁).symm
    _ = m₁ (m₂ e₂ e₁) (m₂ e₁ e₂) := by rw [h₂l, h₂r]
    _ = m₂ (m₁ e₂ e₁) (m₁ e₁ e₂) := interchange e₂ e₁ e₁ e₂
    _ = m₂ e₂ e₂ := by rw [h₁l, h₁r]
    _ = e₂ := h₂l e₂

Axioms used: No axiomsformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

eckmann_hiltonLean 4Proved here from basic factsFormally verified

/-- **The Eckmann–Hilton argument.** Two unital binary operations on the same set that satisfy
the interchange law are equal, and the common operation is commutative. This is the algebra
behind "π₂ is abelian" and behind `endo_id_comm` below. The proof slides `a` and `b` past each
other using the units, exactly as in the lesson's picture of 2-cells moving around each other
in the plane. -/
theorem eckmann_hilton {X : Type*} (m₁ m₂ : X → X → X) (e₁ e₂ : X)
    (h₁l : ∀ a, m₁ e₁ a = a) (h₁r : ∀ a, m₁ a e₁ = a)
    (h₂l : ∀ a, m₂ e₂ a = a) (h₂r : ∀ a, m₂ a e₂ = a)
    (interchange : ∀ a b c d, m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
    (∀ a b, m₁ a b = m₂ a b) ∧ (∀ a b, m₂ a b = m₂ b a) := by
  have he : e₁ = e₂ := units_coincide m₁ m₂ e₁ e₂ h₁l h₁r h₂l h₂r interchange
  subst he
  have same : ∀ a b, m₁ a b = m₂ a b := fun a b =>
    calc m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by rw [h₂r, h₂l]
      _ = m₂ (m₁ a e₁) (m₁ e₁ b) := interchange a e₁ e₁ b
      _ = m₂ a b := by rw [h₁r, h₁l]
  refine ⟨same, fun a b => ?_⟩
  calc m₂ a b = m₁ a b := (same a b).symm
    _ = m₁ (m₂ e₁ a) (m₂ b e₁) := by rw [h₂l, h₂r]
    _ = m₂ (m₁ e₁ b) (m₁ a e₁) := interchange e₁ a b e₁
    _ = m₂ b a := by rw [h₁l, h₁r]

Axioms used: No axiomsformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

eckmann_hilton_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's version: `EckmannHilton.mul_comm` (in `Mathlib.GroupTheory.EckmannHilton`), stated
with Mathlib's `EckmannHilton.IsUnital`. Mathlib uses it to prove that the higher homotopy groups
`πₙ` with `n ≥ 2` are commutative. -/
theorem eckmann_hilton_library {X : Type*} {m₁ m₂ : X → X → X} {e₁ e₂ : X}
    (h₁ : EckmannHilton.IsUnital m₁ e₁) (h₂ : EckmannHilton.IsUnital m₂ e₂)
    (interchange : ∀ a b c d, m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
    ∀ a b, m₂ a b = m₂ b a :=
  (EckmannHilton.mul_comm h₁ h₂ interchange).comm

Axioms used: propext, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

Corollary 3 in an arbitrary bicategory. The proof uses Mathlib's axiom whisker_exchange (the interchange law for whiskerings), the axioms id_whiskerLeft and whiskerRight_id (whiskering by an identity is conjugation by a unitor) and the lemma unitors_equal ( $\lambda_{1_a} = \rho_{1_a}$ ), then cancels the unitor:

endo_id_commLean 4Proved here from basic factsFormally verified

/-- **2-endomorphisms of an identity 1-morphism commute**, in any bicategory: for 2-morphisms
`η θ : 𝟙 a ⟶ 𝟙 a`, `η ≫ θ = θ ≫ η`. This is Eckmann–Hilton inside a bicategory. The two
"operations" are vertical composition and horizontal composition (whiskering), and the
interchange law is Mathlib's axiom `whisker_exchange`. The unitors enter because `𝟙 a ≫ 𝟙 a` is
only isomorphic to `𝟙 a`; the key coherence fact is `λ_(𝟙 a) = ρ_(𝟙 a)` (`unitors_equal`). -/
theorem endo_id_comm {B : Type*} [Bicategory B] {a : B} (η θ : 𝟙 a ⟶ 𝟙 a) :
    η ≫ θ = θ ≫ η := by
  -- Interchange for the two whiskerings of η and θ.
  have ex : 𝟙 a ◁ θ ≫ η ▷ 𝟙 a = η ▷ 𝟙 a ≫ 𝟙 a ◁ θ := whisker_exchange η θ
  -- Whiskering by an identity is conjugation by a unitor; for `𝟙 a` both unitors agree.
  rw [id_whiskerLeft, whiskerRight_id, unitors_equal, unitors_inv_equal] at ex
  -- Now ex : (ρ ≫ θ ≫ ρ⁻¹) ≫ (ρ ≫ η ≫ ρ⁻¹) = (ρ ≫ η ≫ ρ⁻¹) ≫ (ρ ≫ θ ≫ ρ⁻¹).
  simp only [Category.assoc, Iso.inv_hom_id_assoc, cancel_epi] at ex
  -- ex : θ ≫ η ≫ ρ⁻¹ = η ≫ θ ≫ ρ⁻¹; cancel the isomorphism ρ⁻¹ on the right.
  rw [← Category.assoc, ← Category.assoc, cancel_mono] at ex
  exact ex.symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

nat_trans_id_commLean 4Applies a library theoremFormally verified

/-- The special case of `endo_id_comm` in `Cat`: natural transformations from the identity
functor of a category to itself commute. (Their monoid is sometimes called the *centre* of the
category.) This applies Mathlib's `CategoryTheory.NatTrans.id_comm`. -/
theorem nat_trans_id_comm {C : Type*} [Category C] (α β : 𝟭 C ⟶ 𝟭 C) :
    α ≫ β = β ≫ α :=
  NatTrans.id_comm α β

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

The second half of Theorem 4 — every formal diagram of associators and unitors commutes — is in Mathlib in the form "the free bicategory on a quiver is locally thin", proved by normalisation:

free_bicategory_coherenceLean 4Applies a library theoremFormally verified

/-- **Coherence for bicategories**, in the form Mathlib proves it: in the free bicategory on a
quiver `B` (1-morphisms are formal composites of arrows of `B` and identities; 2-morphisms are
built from associators, unitors and their inverses only), any two parallel 2-morphisms are
equal. So every "formal" diagram of associators and unitors commutes, in every bicategory. This
applies Mathlib's instance `CategoryTheory.FreeBicategory.locally_thin` (proved by normalisation,
following Beylin and Dybjer). -/
theorem free_bicategory_coherence {B : Type*} [Quiver B] {a b : FreeBicategory B}
    {f g : a ⟶ b} (η θ : f ⟶ g) : η = θ :=
  Subsingleton.elim η θ

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

Finally, the two halves of "a bicategory with one object is a monoidal category", as Mathlib provides them:

endMonoidalLean 4Formally verified

/-- **A bicategory with one object is a monoidal category**, one direction: the 1-morphisms
`a ⟶ a` of any object `a` form a monoidal category whose tensor product is composition, whose
unit is `𝟙 a`, and whose associator and unitors are those of the bicategory. This is Mathlib's
instance on `CategoryTheory.EndMonoidal`. -/
abbrev endMonoidal {B : Type*} [Bicategory B] (a : B) : MonoidalCategory (a ⟶ a) :=
  inferInstance

Axioms used: propext, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

singleObjEquivLean 4Formally verified

/-- The other direction: a monoidal category `C` becomes a bicategory `MonoidalSingleObj C` with a
single object `⋆`, objects of `C` as 1-morphisms and morphisms of `C` as 2-morphisms; and the
monoidal category of endomorphisms of `⋆` is equivalent to `C` again. This is Mathlib's
`CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence`. -/
noncomputable def singleObjEquiv (C : Type*) [Category C] [MonoidalCategory C] :
    EndMonoidal (MonoidalSingleObj.star C) ≌ C :=
  MonoidalSingleObj.endMonoidalStarFunctorEquivalence C

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HigherCategories.leanTry it in the Lean web editor

What is not formalised. The first half of Theorem 4 (every bicategory is biequivalent to a strict 2-category), tricategories and Gray-categories (Theorem 5), Simpson's theorem, and any definition of weak $n$ -category for $n \ge 3$ are not formalised here, and as far as we know not in Mathlib. Mathlib's coherence tactics (coherence, bicategory) put the locally-thin theorem to work: they prove equations between structural 2-cells automatically.

ComputationC

The shape of coherence: associahedra

Bracketings of a word of $n$ letters, joined when they differ by one associator, form the 1-skeleton of Stasheff's associahedron $K_n$ . The experiment builds these graphs for $n \le 7$ , checks that they are connected (any two bracketings are related by associators), finds Mac Lane's pentagon as the two directed paths of lengths 2 and 3 in $K_4$ , and computes that the 2-dimensional faces of $K_5$ are 6 pentagons and 3 squares whose boundaries span every cycle (mod 2). The squares are the "naturality" relations between associators acting on disjoint parts of the word; the pentagons are instances of the pentagon axiom. This is the combinatorial content of the second half of Theorem 4.

Associahedra: bracketings, associators and the pentagonPythonExact computationExhaustive finite checkComputationally tested

"""Associahedra: the shapes of coherence for associativity, computed exactly.

In a bicategory (or monoidal category) composition is associative only up to
associator 2-cells. The bracketings of a word of n letters are the vertices of
a graph whose edges are single associator moves ((xy)z) <-> (x(yz)); it is the
1-skeleton of Stasheff's associahedron K_n. We enumerate it exhaustively for
small n and check: the number of bracketings is a Catalan number; the graph is
connected (any two bracketings are related by associators); the two directed
paths from the left comb to the right comb for n = 4 have lengths 2 and 3 (the
two sides of Mac Lane's pentagon); and for n = 5 the 2-dimensional faces are 6
pentagons and 3 squares, with V - E + F = 2, and their boundaries span the
cycle space mod 2 (every loop of associators is a sum of faces). This is
exact, exhaustive-finite evidence for these n only; coherence for all n is
Mac Lane's theorem.
"""

from collections import deque
from math import comb

def bracketings(letters):
    """All full bracketings of a tuple of letters, as nested pairs."""
    if len(letters) == 1:
        return [letters[0]]
    out = []
    for i in range(1, len(letters)):
        for left in bracketings(letters[:i]):
            for right in bracketings(letters[i:]):
                out.append((left, right))
    return out

def show(t):
    """Write a bracketing as a string, e.g. ((ab)c)d."""
    if isinstance(t, str):
        return t
    a, b = (show(x) if isinstance(x, str) else "(" + show(x) + ")" for x in t)
    return a + b

def moves(t, forward_only=False):
    """Bracketings one associator away from t.

    The forward move is ((x y) z) -> (x (y z)); without ``forward_only`` the
    inverse move (x (y z)) -> ((x y) z) is included too.
    """
    if isinstance(t, str):
        return []
    left, right = t
    out = [(m, right) for m in moves(left, forward_only)]
    out += [(left, m) for m in moves(right, forward_only)]
    if not isinstance(left, str):
        out.append((left[0], (left[1], right)))
    if not forward_only and not isinstance(right, str):
        out.append(((left, right[0]), right[1]))
    return out

def associator_graph(n):
    """Vertices (bracketings of n letters) and undirected edges of K_n."""
    vertices = bracketings(tuple("abcdefgh"[:n]))
    edges = {frozenset((v, w)) for v in vertices for w in moves(v)}
    return vertices, edges

def distances(start, step):
    """Breadth-first distances from ``start`` along the neighbour map ``step``."""
    dist = {start: 0}
    queue = deque([start])
    while queue:
        v = queue.popleft()
        for w in step(v):
            if w not in dist:
                dist[w] = dist[v] + 1
                queue.append(w)
    return dist

def comb_bracketing(n, left=True):
    """The left comb ((ab)c)d... or the right comb a(b(c(d...)))."""
    letters = "abcdefgh"[:n]
    if left:
        t = letters[0]
        for x in letters[1:]:
            t = (t, x)
        return t
    t = letters[-1]
    for x in reversed(letters[:-1]):
        t = (x, t)
    return t

def directed_path_lengths(n):
    """Lengths of all directed paths left comb -> right comb (forward moves)."""
    memo = {}

    def lengths(t):
        if t not in memo:
            nxt = moves(t, forward_only=True)
            memo[t] = {0} if not nxt else {1 + k for s in nxt for k in lengths(s)}
        return memo[t]

    return sorted(lengths(comb_bracketing(n, left=True)))

def contains_block(t, block):
    """Does bracketing t contain a bracket around exactly the letters ``block``?"""
    if isinstance(t, str):
        return False
    if leaves(t) == block:
        return True
    return contains_block(t[0], block) or contains_block(t[1], block)

def leaves(t):
    """The letters of a bracketing, in order, as a string."""
    return t if isinstance(t, str) else leaves(t[0]) + leaves(t[1])

def facets(n):
    """Facets of K_n: for each proper block of >= 2 consecutive letters, the
    set of bracketings that bracket that block (a list of vertex sets)."""
    word = "abcdefgh"[:n]
    vertices = bracketings(tuple(word))
    out = []
    for r in range(2, n):
        for i in range(n - r + 1):
            block = word[i:i + r]
            out.append({v for v in vertices if contains_block(v, block)})
    return out

def gf2_rank(vectors):
    """Rank over GF(2) of vectors given as Python integers (bit masks)."""
    basis = {}
    for v in vectors:
        while v:
            top = v.bit_length() - 1
            if top not in basis:
                basis[top] = v
                break
            v ^= basis[top]
    return len(basis)

def face_boundary_rank(n):
    """GF(2) rank of the boundaries of the 2-faces of K_n, for n = 5.

    Each face is given by its vertex set; its boundary is the set of edges of
    K_n with both ends in the face, encoded as a bit mask over the edges.
    """
    vertices, edges = associator_graph(n)
    index = {e: i for i, e in enumerate(sorted(edges, key=sorted_key))}
    masks = []
    for face in facets(n):
        mask = 0
        for e in edges:
            if e <= face:
                mask |= 1 << index[e]
        masks.append(mask)
    return gf2_rank(masks)

def sorted_key(edge):
    """A deterministic sort key for an undirected edge."""
    return sorted(show(v) for v in edge)

def main():
    print(" n  bracketings  Catalan  edges  connected  diameter  cycle rank")
    for n in range(3, 8):
        vertices, edges = associator_graph(n)
        nbrs = {v: set(moves(v)) for v in vertices}
        reach = distances(vertices[0], nbrs.__getitem__)
        diameter = max(max(distances(v, nbrs.__getitem__).values())
                       for v in vertices)
        catalan = comb(2 * (n - 1), n - 1) // n
        rank = len(edges) - len(vertices) + 1
        print(f"{n:>2} {len(vertices):>12} {catalan:>8} {len(edges):>6} "
              f"{str(len(reach) == len(vertices)):>10} {diameter:>9} "
              f"{rank:>11}")
    print()
    print("Directed paths ((ab)c)d -> a(b(cd)) have lengths",
          directed_path_lengths(4))
    print("  (the two sides of Mac Lane's pentagon).")
    print("n = 5: directed path lengths left comb -> right comb:",
          directed_path_lengths(5))
    sizes = [len(face) for face in facets(5)]
    v5, e5 = associator_graph(5)
    print(f"K_5 faces: {sizes.count(5)} pentagons, {sizes.count(4)} squares; "
          f"V - E + F = {len(v5)} - {len(e5)} + {len(sizes)} = "
          f"{len(v5) - len(e5) + len(sizes)}")
    print(f"GF(2) rank of the face boundaries: {face_boundary_rank(5)} = cycle "
          f"rank {len(e5) - len(v5) + 1}: mod 2,")
    print("every loop of associators is a sum of pentagons and squares.")
    print()
    print("Epistemic status: exact, exhaustive enumeration for n <= 7 (faces for")
    print("n = 5 only). It illustrates, but does not prove, Mac Lane's coherence")
    print("theorem, which says every diagram of associators commutes for every n.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Explore

Explore: the pentagon and the associahedron K₅

The pentagon axiom asserts that the two composites of associators from $((kh)g)f$ to $k(h(gf))$ are equal:

Mac Lane's pentagon. Juxtaposition is composition of 1-cells; every arrow is an invertible 2-cell.

For five letters there are 14 bracketings. Below they are the vertices of the associahedron $K_5$ , numbered as in this table (with $e$ the fifth 1-cell); edges are single associator moves.

#	bracketing	#	bracketing	#	bracketing
1	$a(b(c(de)))$	6	$(ab)(c(de))$	11	$(a((bc)d))e$
2	$a(b((cd)e))$	7	$(ab)((cd)e)$	12	$((ab)(cd))e$
3	$a((bc)(de))$	8	$(a(bc))(de)$	13	$((a(bc))d)e$
4	$a((b(cd))e)$	9	$((ab)c)(de)$	14	$(((ab)c)d)e$
5	$a(((bc)d)e)$	10	$(a(b(cd)))e$

The associahedron K₅

Vertices: bracketings of abcde. Edges: one associator.

|V| = 14|E| = 21Click edges one after another to walk along them, or pick a starting vertex first.

No walk yet.

14 vertices have odd degree: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14.

So no Euler trail is possible. A trail enters and leaves each vertex in its middle in pairs, so only its two ends can have odd degree, and this graph has 14 such vertices.

Things to try:

In degrees mode, check that every vertex has degree 3: a bracketing of five letters has three internal brackets, and each allows exactly one associator move.
The outer pentagon $14 \to 12 \to 10$ and $14 \to 13 \to 11 \to 10$ is Mac Lane's pentagon for $abcd$ , followed by $e$ . Find the other five pentagons and the three squares (for example the square $1, 2, 7, 6$ : the associator inside the block $cde$ and the associator $a(bX) \Rightarrow (ab)X$ with $X = cde$ act on disjoint parts of the word, so they commute — a naturality square).
In walk mode, build a closed walk. Each step is an associator or its inverse, so the walk composes to a 2-cell from a bracketing to itself. Coherence says it is always the identity — because every closed walk is filled in by faces.

Exercises

1. Higher categories

Warm-upHuman

A bicategory with exactly one object $\star$ is the same thing as which of the following?

Choose one

A monoidal category: the 1-cells

\star \to \star

are its objects, the 2-cells its morphisms, and horizontal composition its tensor productA monoidA commutative monoidA groupoid

2. Higher categories

Warm-upComputational

How many ways are there to fully bracket a composite of six composable 1-cells $f_6 f_5 f_4 f_3 f_2 f_1$ ? (These are the vertices of the associahedron $K_6$ .)

3. Higher categories

CoreHuman

Let $\alpha : F \Rightarrow G$ (functors $\mathcal{C} \to \mathcal{D}$ ) and $\gamma : I \Rightarrow J$ (functors $\mathcal{D} \to \mathcal{E}$ ). Which formulas give the component $(\gamma \ast \alpha)_X : IFX \to JGX$ of the horizontal composite? (Choose all that apply.)

Choose all that apply

J(\alpha_X) \circ \gamma_{FX}

\gamma_{GX} \circ I(\alpha_X)

\gamma_{X} \circ \alpha_X

I(\alpha_X) \circ \gamma_{GX}

4. Higher categories

CoreHuman

In the proof of the interchange law $(\delta \cdot \gamma) \ast (\beta \cdot \alpha) = (\delta \ast \beta) \cdot (\gamma \ast \alpha)$ in $\mathbf{Cat}$ , after expanding components the two sides are $K(\beta_X) K(\alpha_X) \delta_{FX} \gamma_{FX}$ and $K(\beta_X)\, \delta_{GX} J(\alpha_X)\, \gamma_{FX}$ . Which fact finishes the proof?

Choose one

Naturality of

\delta

at the morphism

\alpha_X

Naturality of

\alpha

Functoriality of

K

aloneAssociativity of composition in

\mathcal{E}

5. Higher categories

CoreHuman

The Eckmann–Hilton argument assumes that both operations are unital. Which pair of operations on a set with at least two elements satisfies the interchange law $(a \star b) \odot (c \star d) = (a \odot c) \star (b \odot d)$ but is not commutative, showing the unit hypothesis cannot be dropped?

Choose one

a \odot b = a

and

a \star b = a

(both are 'left projection')

\odot = \star = +

on

\Z

\odot = \star =

matrix multiplication on

2 \times 2

matrices

a \odot b = a + b

and

a \star b = ab

on

\Z

6. Higher categories

CoreFormal

Let B be a bicategory in Lean ([Bicategory B]) and a : B. Which statement formalises Corollary 3, 'the 2-endomorphisms of an identity 1-morphism commute'?

Choose one

∀ η θ : 𝟙 a ⟶ 𝟙 a, η ≫ θ = θ ≫ η∀ f g : a ⟶ a, f ≫ g = g ≫ f∀ (f : a ⟶ a) (η θ : f ⟶ f), η ≫ θ = θ ≫ η∀ η θ : 𝟙 a ⟶ 𝟙 a, η ▷ 𝟙 a = 𝟙 a ◁ θ

7. Higher categories

CoreHuman

Which of these are strict 2-categories, with composition of 1-cells associative and unital on the nose? (Choose all that apply.)

Choose all that apply

Categories, functors and natural transformationsSets, spans of sets (composed by pullback) and maps of spansRings, bimodules (composed by tensor product) and bimodule mapsThe one-object 2-category of a strict monoidal category, e.g. endofunctors of a category under composition

8. Higher categories

StretchHuman

Which statement about coherence in dimension 3 is correct?

Choose one

Every tricategory is triequivalent to a Gray-category, but not every tricategory is triequivalent to a strict 3-category.Every tricategory is triequivalent to a strict 3-category, as in dimension 2.No coherence theorem is known for tricategories.Coherence already fails for bicategories: not every bicategory is biequivalent to a strict 2-category.

9. Higher categories

StretchComputational

Write count_bracketings(n), the number of full bracketings of a word of n letters (use the recursion over the outermost bracket), and count_moves(n), the number of edges of the associahedron $K_n$ : pairs of bracketings that differ by one associator. Use the fact that every bracketing of $n \ge 2$ letters has exactly $n - 2$ internal brackets, each allowing exactly one associator move.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Strictification works in every dimension, so weak structures are just strict ones written sloppily." It works in dimension 2 (Theorem 4) and fails in dimension 3: by Gordon–Power–Street, tricategories can be strictified only to Gray-categories, and Simpson showed that the homotopy 3-type of $S^2$ is not modelled by a strict 3-groupoid. Weakness carries genuine information.

Misconception

"There is one agreed definition of weak $n$ -category." There are many (Leinster's 2002 survey describes ten), they are known to agree in low dimensions and in important homotopical cases, and comparing them in general is ongoing research. Results should always say which definition they use.

Misconception

"Strictification lets you assume the bicategory you started with is strict." Theorem 4 replaces $\mathcal{B}$ by a biequivalent strict 2-category, which usually has different objects and 1-cells. For example, composition of spans is defined only up to isomorphism, and no choice of pullbacks makes it strictly associative in general. You may reason in the strict model and transport the conclusion, but you may not pretend the associators of $\mathcal{B}$ are identities.

Misconception

"Eckmann–Hilton says 2-cells in a 2-category commute." Only the endomorphisms of an identity 1-cell $1_a$ are forced to commute. For a general 1-cell $f$ the monoid of 2-cells $f \Rightarrow f$ can be any monoid: in $\mathbf{Cat}$ , take $f$ to be a functor from the terminal category picking out an object $X$ ; its natural endomorphisms are the monoid $\mathrm{End}(X)$ , which can be non-commutative.

Misconception

"The pentagon is the only axiom." A bicategory also needs the triangle axiom relating associators and unitors, and the associator and unitors must be natural. Without the triangle, the coherence theorem fails.

ViewpointsH

Many ways of seeing

Topology— Homotopy types and the homotopy hypothesis

Every space $X$ has a fundamental $n$ -groupoid $\Pi_n(X)$ : points, paths, homotopies between paths, …, with $n$ -cells taken up to homotopy. Grothendieck's homotopy hypothesis (in Pursuing Stacks, 1983) proposes that weak $n$ -groupoids are "the same as" homotopy $n$ -types. In dimension 1 this is a theorem: the homotopy category of 1-types is equivalent to the homotopy category of groupoids. In dimension 2 it is also established, and connected pointed 2-types correspond to crossed modules (Mac Lane and Whitehead, 1950). The Eckmann–Hilton argument is the topological fact that you can move two small discs past each other in the plane; Simpson's theorem is the fact that you cannot model the Hopf map with strict interchange. For an ∞-groupoid version see ∞-categories and Homotopy theory.

Geometry— String diagrams: 2-cells live in the plane

In the Poincaré dual picture of a 2-category, 0-cells are regions of the plane, 1-cells are lines between regions and 2-cells are points (beads) on lines. Vertical composition stacks diagrams, horizontal composition places them side by side, and the interchange law is the statement that planar isotopy — sliding beads up and down past each other on different strings — does not change the value of a diagram. Joyal and Street (1991) made this precise for monoidal categories: a well-formed equation follows from the axioms exactly when the corresponding diagrams are isotopic. Braided monoidal categories need three dimensions (strings may pass over and under), which is where knots and braids enter: see Knot theory.

Algebra— Categorification and 2-groups

Higher categories turn equations into isomorphisms: this is categorification. A group becomes a 2-group, a monoidal category in which every object and every morphism is invertible; 2-groups are classified up to equivalence by a group $G$ , an abelian group $A$ with a $G$ -action, and a class in $H^3(G; A)$ (Sinh, 1975). Categorified representation theory replaces vector spaces by linear categories and linear maps by functors; Khovanov homology categorifies the Jones polynomial and Chuang and Rouquier's $\mathfrak{sl}_2$ -categorification proved Broué's abelian defect group conjecture for symmetric groups (2008). See Categorical representation theory.

Physics— Extended topological field theories

Atiyah's axioms (1988) describe an $n$ -dimensional topological quantum field theory as a symmetric monoidal functor from a category of $(n-1)$ -manifolds and $n$ -dimensional cobordisms to vector spaces. Physical locality suggests going further down: cutting a manifold along codimension-2 pieces, and so on to points, which requires an $n$ -category of cobordisms with corners. Baez and Dolan's cobordism hypothesis (1995) predicts that fully extended framed TQFTs are classified by their value on a point, which must be a "fully dualisable" object. Lurie (2009) gave a detailed outline of a proof in the language of $(\infty, n)$ -categories; supplying every detail has been the subject of substantial later work. The heuristic (locality in physics) and the theorem (about $(\infty, n)$ -categories) should be kept apart. See Gauge theory.

Category theory— Enrichment and the 2-category of categories

A strict 2-category is precisely a category enriched in $(\mathbf{Cat}, \times)$ : hom-objects are categories and composition is a functor (see Enriched categories). A bicategory is the "weak" version, and iterating — enriching in the category of $n$ -categories — gives strict $(n+1)$ -categories, which is why strict definitions are easy and weak ones hard. Much of ordinary category theory is really 2-category theory in $\mathbf{Cat}$ : adjunctions, monads and Kan extensions can be defined in any 2-category, and Street's "formal theory of monads" (1972) does exactly that.

Wonder Trails

Wonder Trail · Optional · never gradedArrows that composeWhat do functions between sets, maps between groups and continuous maps between shapes have in common? What if we studied only the arrows?Follow the trail

History & global context

History and global context

1950s–1960s: higher structure appears. Mac Lane and Whitehead (1950) classified homotopy 2-types by crossed modules. Eckmann and Hilton published their argument in 1962. Stasheff (1963) introduced the associahedra to describe homotopy-associative H-spaces, and in the same year Mac Lane proved coherence for monoidal categories. Charles Ehresmann (France) introduced double categories and 2-categories in the early 1960s.
1967: bicategories. Jean Bénabou's Introduction to bicategories defined bicategories, with spans as the motivating example.
1970s–1980s: the Sydney school and Grothendieck. Ross Street and Max Kelly in Australia developed 2-category theory (the formal theory of monads, 1972; Kelly–Street's Review of the elements of 2-categories, 1974). Street's "orientals" (1987) proposed a simplicial approach to $\omega$ -categories. Grothendieck's long letter-manuscript Pursuing Stacks (1983) set out the homotopy hypothesis.
1990s: dimension 3 and beyond. Gordon, Power and Street defined tricategories (1995). Kapranov and Voevodsky (1991) claimed that strict ∞-groupoids model all homotopy types; Simpson (1998) showed that the 3-type of $S^2$ is not modelled by a strict 3-groupoid. Voevodsky later described this episode as one of the motivations for his work on computer-checked proofs (see Homotopy type theory). Baez and Dolan (1995) formulated the periodic table, the stabilization hypothesis and the cobordism hypothesis; Batanin (1998) gave a definition of weak $\omega$ -category via globular operads, and Tamsamani (1999) and Simpson developed Segal-type definitions.
2000s–today. Leinster's survey (2002) and book (2004) organised the definitions; Lurie's work on $(\infty, n)$ -categories (2009) and many others moved the subject into homotopy theory; textbooks on 2-dimensional categories (Johnson–Yau, 2021) consolidated dimension 2.

Why go up a dimension?

Cells, pasting and the two compositions

2-categories, bicategories and pseudofunctors

Examples and non-examples

Central theorems

The landscape: what is known and what is open

Higher categories in Lean and Mathlib

The shape of coherence: associahedra

Explore: the pentagon and the associahedron K₅

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading