Skip to Main Content

Could -Category Theory Be Taught to Undergraduates?

Emily Riehl

Communicated by Notices Associate Editor Steven Sam

Article cover

1. The Algebra of Paths

It is natural to probe a suitably nice topological space by means of its paths, the continuous functions from the standard unit interval to . But what structure do the paths in form?

To start, the paths form the edges of a directed graph whose vertices are the points of : a path defines an arrow from the point to the point . Moreover, this graph is reflexive, with the constant path at each point defining a distinguished endoarrow.

Can this reflexive directed graph be given the structure of a category? To do so, it is natural to define the composite of a path from to and a path from to by gluing together these continuous maps—i.e., by concatenating the paths—and then by reparametrizing via the homeomorphism that traverses each path at double speed:

But the composition operation fails to be associative or unital. In general, given a path from to , the composites and are not equal: while the have the same image in , their parametrizations differ. However, they are based homotopic, in the sense that there exists a continuous function so that

a situation we summarize by writing . Similarly, the paths are all based homotopic, though not equal (unless is the constant path).

Paths are also invertible up to based homotopy: for any path from to , its reversal , defined by precomposing with the flipping automorphism , defines an inverse up to based homotopy: and . These observations motivate the following definition:

Definition 1.2.

For a space , the fundamental groupoid is the category whose:

objects are the points of and

arrows are based homotopy classes of paths of

with composition defined by concatenation, identity arrows defined by the constant paths, and inverses defined by reversing paths.

The fundamental groupoid of a space answers a slightly different question than originally posed, describing the structure formed by the based homotopy classes of paths in . The paths themselves form something like a weak groupoid where composition is not uniquely defined. Indeed, given paths from to and from to , the composite in is represented by any path so that there is a based homotopy witnessing . Here, the based homotopy defines a continuous function from the solid 2-simplex into that restricts along the boundary triangle to the map defined by gluing the three paths:

While multivalued composition operations are not well-behaved in general, this one has a certain homotopical uniqueness property: the witnessing homotopies for two such composites can be glued together—by a higher-dimensional analogue of the construction 1.1—to define a homotopy . This suggests that the witnessing homotopies that fill the triangles formed by the paths between and and might be productively regarded as part of the composition data. Thus, the moduli space of composites of and is defined as follows:

Definition 1.3.

Given composable paths and in a space , the space of composites of and is the subspace of continuous maps that restrict on the boundary horn to :

The homotopical uniqueness of path composition can be strengthened by the following observation:

Theorem 1.5.

For any composable paths and in a space , the space of composites is contractible.

So what do the paths in form? We have seen that they form a weak groupoid with a multivalued but homotopically unique composition law. In fact, this weak category is an infinite-dimensional category. The based homotopies between parallel paths and themselves might be regarded as paths between points and in the space to which Theorem 1.5 equally applies, and these observations extend iteratively to higher-dimensional homotopies. The points, paths, and higher paths in a space assemble into a weak infinite-dimensional category—with interacting weak composition and identities for paths at all levels⁠Footnote1—in which all morphisms are weakly invertible. Such a structure is known as an -groupoid.


Famously, the definition of a weak 3-dimensional category by Gordon, Power, and Street takes six pages to state.

The homotopy hypothesis

The fundamental -groupoid of paths in captures the data of all of the higher homotopy groups of the space, information which is referred to as the homotopy type of the space. In a famous letter to Quillen G, Grothendieck formulated his homotopy hypothesis, positing that the fundamental -groupoid construction defines an equivalence between homotopy types and -groupoids. Grothendieck’s vision was that this result should be provable for various models of -groupoids that were then under development, though some instead use this thesis to define an -groupoid to be a homotopy type.

There is something unsatisfying, though, about the naïve interpretation of the homotopy hypothesis as the assertion of a bijection between the collection of homotopy types and the collection of -groupoids, or even as an equivalence between the homotopy category of spaces⁠Footnote2 and the homotopy category of -groupoids. The disappointment lies in the fact that both spaces and -groupoids live most naturally as the objects in weak infinite-dimensional categories, with the standard morphisms between them supplemented by higher-dimensional weakly invertible morphisms. Thus, a more robust expression of the homotopy hypothesis is the assertion that the -categories of spaces and of -groupoids are equivalent,⁠Footnote3 so now we must explain what -categories are.


Homotopy types can be understood as isomorphism classes of objects in the homotopy category of spaces, the category obtained by localizing the category of spaces and continuous functions by the weak homotopy equivalences, those functions that induce isomorphisms on all homotopy groups.


In fact, a version of this result had been proven already by Quillen for the Kan complex model of -groupoids Q, but this was not so clearly understood at the time.

2. -Categories in Mathematics

Over the past few decades, -categories—weak infinite-dimensional categories with weakly invertible morphisms above dimension one—have been invading certain areas of mathematics. In derived algebraic geometry, the derived category of a ring is now understood as the 1-categorical quotient of the -category of chain complexes, and an -categorical property called “stability” explains the triangulated structure borne by the derived category. In mathematical physics, Atiyah’s topological quantum field theories have been “extended up” to define functors between -categories.⁠Footnote4 -categories have also made appearances in the Langlands program in representation theory and in symplectic geometry among other areas. Quillen’s model categories Q from abstract homotopy theory are now understood as presentations of -categories.


Lurie’s “fully extended” topological quantum field theories are also “extended down” so that they might be understood as functors between -categories, with non-invertible morphisms up to and including the dimension of the indexing cobordisms. Here we reserve the term -categories” for -categories,” which have non-invertible morphisms only in the bottom dimension.

Ordinary categories “frame a template for a mathematical theory,” with the objects providing the “nouns” and the morphisms the “verbs,” in a metaphor suggested by Mazur. As the objects mathematicians study increase in complexity, a more robust linguistic template may be required to adequately describe their natural habitats—with adjectives, adverbs, pronouns, prepositions, conjunctions, interjections, and so on—leading to the idea of an -category. Like an ordinary 1-category, an -category has objects and morphisms, now thought of as “1-dimensional” transformations. The extra linguistic color is provided by higher-dimensional invertible morphisms between morphisms—such as chain homotopies or diffeomorphisms—and higher morphisms between these morphisms, continuing all the way up.

How might a researcher in one of these areas go about learning this new technology of -categories? And how might -category theory ultimately be distilled down into something that we could reasonably teach advanced undergraduates of the future?

Curiosities from the literature

-categories were first introduced by Boardman and Vogt to describe the composition structure of homotopy coherent natural transformations between homotopy coherent diagrams BV. Joyal was the first to assert that “most concepts and results of category theory can be extended to [-categories]” and pioneered the development of -categorical analogues of standard categorical notions J. Lurie then developed various aspects of -category theory that were needed for his thesis on derived algebraic geometry L1. His books L2L3 and the online textbook Kerodon are primary references for uses of this technology, while texts written by Cisinski, Groth, Hinich, Rezk, and others provide parallel introductions to the field.

If one delves further into the -categories literature, some curiosities soon become apparent:


Particularly in talks or lecture series introducing the subject, the definition of -category is frequently delayed, and when definitions are given, they don’t always agree.

These competing definitions are referred to as models of -categories, which are Bourbaki-style mathematical structures defined in terms of sets and functions that represent infinite-dimensional categories with a weak composition law in which all morphisms above dimension one are weakly invertible. In order of appearance, these include simplicial categories, quasi-categories, relative categories, Segal categories, complete Segal spaces, and 1-complicial sets, each of which comes with an associated array of naturally occurring examples Be.


Considerable work has gone into defining the key notions for and proving the fundamental results about -categories, but sometimes this work is later redeveloped starting from a different model.

For instance, KV begins:

In recent years -categories or, more formally, ,1)-categories appear in various areas of mathematics. For example, they became a necessary ingredient in the geometric Langlands problem. In his books L2L3 Lurie developed a theory of -categories in the language of quasi-categories and extended many results of the ordinary category theory to this setting.

In his work R1 Rezk introduced another model of -categories, which he called complete Segal spaces. This model has certain advantages. For example, it has a generalization to -categories (see R2).

It is natural to extend results of the ordinary category theory to the setting of complete Segal spaces. In this note we do this for the Yoneda lemma.


Alternatively, authors decline to pick a model at all and instead work “model-independently.”

One instance of this appears in the precursor L1 to L2, which avoids selecting a model of -categories at all:

We will begin in §1 with an informal review of the theory of -categories. There are many approaches to the foundation of this subject, each having its own particular merits and demerits. Rather than single out one of those foundations here, we shall attempt to explain the ideas involved and how to work with them. The hope is that this will render this paper readable to a wider audience, while experts will be able to fill in the details missing from our exposition in whatever framework they happen to prefer.

The fundamental obstacle to giving a uniform definition of an -category is that our traditional set-based foundations for mathematics are not really suitable for reasoning about -categories: sets do not feature prominently in -categorical data, especially when -categories are only well-defined up to equivalence, as they must be when different models are involved. When considered up to equivalence, -categories, like ordinary categories, do not have a well-defined set of objects. Essentially, -categories are 1-categories in which all the sets have been replaced by -groupoids. Where a category has a set of elements, an -category has an -groupoid of elements, and where a category has hom-sets of morphisms, -categories have -groupoidal mapping spaces.⁠Footnote5 The axioms that turn a directed graph into a category are expressed in the language of set theory: a category has a composition function satisfying axioms expressed in first-order logic with equality. By analogy, composition in an -category can be understood as a morphism between -groupoids, but such morphisms no longer define functions since homotopy types do not have underlying sets of points.⁠Footnote6 This is why there is no canonical model of -categories.


“Large” -categories also exist and behave like large 1-categories.


Similar considerations have motivated Scholze et al to use the term “anima”—referring to the “soul” of a “space”—as a synonym for -groupoids.

Reimagining the foundations of -category theory

Despite these subtleties, it is possible to reason rigorously and model-independently about -categories without getting bogged down in the combinatorial scaffolding of a particular model. The framework introduced in §3 considerably streamlines the basic core theory of -categories, though its scope is currently more limited than the corpus of results that have been proven using a model.

However, this current state of the art employs proof techniques that are unfamiliar to non-category theorists and thus is not feasible to integrate into the undergraduate curriculum. The concluding §4 describes a more speculative dream for the future where enhancements to the foundations of mathematics would allow us to interpret uniqueness as contractibility and automatically ensure that all constructions are invariant under equivalence.

3. The Formal Theory of -Categories

In the paper “General theory of natural equivalences” that marked the birth of category theory, Eilenberg and Mac Lane observed that categories, functors, and natural transformations assemble into a 2-category . The essence of this result is the observation that natural transformations can be composed in 2-dimensions’ worth of ways: “vertically” along a boundary functor or “horizontally” along a boundary category.

More generally, Power proves that any pasting diagram of compatibly oriented functors and natural transformations has a unique composite.

The pasting composite, which in the example above defines a natural transformation between the categories and from the functor to the functor , can be decomposed as a vertical composite of whiskerings of the atomic natural transformations : for instance, the composite factors as followed by followed by followed by followed by , among eight total possibilities. Power’s theorem is that pasting composition is well-defined.

Similarly, in well-behaved models of -categories:

Proposition 3.1 (Joyal, Riehl–Verity).

-categories, -functors, and -natural transformations assemble into a cartesian closed 2-category .

This result was first observed in the quasi-category model by Joyal J. Since the category of quasi-categories is cartesian closed, it is enriched over itself, defining an -category of quasi-categories. The 2-category of quasi-categories is obtained by a quotienting process, that maps each hom-quasi-category to its homotopy category, by applying the left adjoint to the (nerve) inclusion of categories into quasi-categories. The other “well-behaved” models—including complete Segal spaces, Segal categories, and 1-complicial sets among others—are also cartesian closed, so a similar construction defines a 2-category of complete Segal spaces, and so on.⁠Footnote7 To adopt a “model-independent” point of view, note that these 2-categories are all biequivalent or “the same” in the sense appropriate to 2-category theory RV2, §E.2.


While the meaning of the terms -categories” and -functors” in a given model is typically clear, the -natural transformations,” which can be understood as equivalence classes of 2-cells in the ambient -category, are less evident.

The good news, which is surprising to many experts, is that a fair portion of the basic theory of -categories can be developed in the 2-category . These aspects might be described as formal category theory, as they involve definitions of categorical notions such as equivalence, adjunction, limit, and colimit that can be defined internally to any 2-category. In the 2-category , these recover the classical notions from 1-category theory, while in the 2-category these specialize to the correct notions in -category theory.⁠Footnote8 Thus, for the core basic theory involving these notions, ordinary category theory extends to -categories simply by appending the prefix RV2, §2-4.


The technical part of this story involves proofs that the “synthetic” or “formal” notions introduced here agree with the previously-defined “analytic” notions in the quasi-categories model RV2, §F. But we encourage those not already acquainted with the analytic theory of some model of -categories to learn these definitions first.

Equivalences and adjunctions

The following definitions make sense in an arbitrary cartesian closed 2-category, such as .

Definition 3.2.

An equivalence between -categories is given by:

a pair of -categories and ,

a pair of -functors and , and

a pair of invertible -natural transformations , and .

Definition 3.3.

An adjunction between -categories is given by:

a pair of -categories and ,

a pair of -functors and , and

a pair of -natural transformations and

so that the following pasting identities hold:

One commonly writes to indicate that is left adjoint to , its right adjoint, with the data of the unit and counit being left implicit.

Among the many advantages of using definitions that are taken “off the shelf” from the 2-categories literature is that the standard 2-categorical proofs then specialize to prove the following facts about adjunctions between -categories.⁠Footnote9


What is less obvious is that these definitions are “correct” for -category theory. In the case of equivalences, this is easily seen in any of the models. In the case of adjunctions, this is quite subtle, and involves the fact that the low-dimensional data enumerated in Definition 3.3 suffices to determine a full “homotopy coherent adjunction,” uniquely up to a contractible space of choices RV1.

Proposition 3.4 (RV2, 2.1.9).

Adjunctions between -categories compose:

Proposition 3.5 (RV2, 2.1.10).

Given an adjunction between -categories and a functor , is left adjoint to if and only if there exists a natural isomorphism .

Proposition 3.6 (RV2, 2.1.12).

Any equivalence can be promoted to an adjoint equivalence at the cost of replacing either of the natural isomorphisms.

Relative adjunctions

The unit and counit in an adjunction satisfy a universal property in the 2-category that we now explore in the case of the counit . Given any -functors and , pasting with defines a bijection between -natural transformations and . Any factors through a unique as displayed below:

which is to say that the pair defines an absolute right lifting of through . Indeed, is left adjoint to with counit if and only if defines an absolute right lifting of through RV2, 2.3.7.

Any component of the counit of an adjunction satisfies a universal property analogous to 3.7:

which asserts that defines an absolute right lifting of through . Motivated by examples such as these, absolute right liftings of a generic -functor through can be thought of as exhibiting as right adjoint to relative to with partial counit .

Definition 3.8.

Given -functors and with common codomain, a functor and -natural transformation define an absolute right lifting of through or a right adjoint of relative to if pasting with induces a bijection between -natural transformations as displayed below:

The following lemmas about relative right adjoints admit straightforward 2-categorical proofs:

Lemma 3.9 (RV2, 2.3.6).

If is right adjoint to relative to then for any , is right adjoint to relative to .

Lemma 3.10 (RV2, 2.4.1).

Suppose that is right adjoint to relative to . Then in any diagram of -functors and -natural transformations

is right adjoint to relative to if and only if is right adjoint to relative to .

Limits and colimits

Relative adjunctions can be used to define limits and colimits of diagrams valued inside an -category and indexed by another -category . As a cartesian closed 2-category, contains a terminal -category , which admits a unique -functor from any other -category . Maps from the terminal -category into another -category define elements in the -category .⁠Footnote10 Using the cartesian closed structure, any diagram defines an element in the -category of -shaped diagrams in . Exponentiation with the unique functor defines the constant diagrams functor , which carries an element of to the constant -shaped diagram at that element.


We find this terminology less confusing than referring to the “objects” in an -category , which is itself an object of .

Definition 3.11.

An -category admits -shaped limits if the constant diagrams functor admits a right adjoint and admits -shaped colimits if the constant diagrams functor admits a left adjoint:

The counit of the adjunction and the unit of the adjunction encode the limit and colimit cones, as is most easily seen when considering their components at a diagram . By Lemma 3.9, the right and left adjoints restrict to define relative adjunctions:

These observations allow us to generalize Definition 3.11 to express the universal properties of the limit or colimit of a single diagram in settings where the limit and colimit functors do not exist.

Definition 3.12.

A diagram between -categories admits a limit just when admits a relative right adjoint at and admits a colimit just when admits a relative left adjoint at , as encoded by absolute lifting diagrams:

There is an easy formal proof of the -categorical version of a classical theorem:

Theorem 3.13.

Right adjoints preserve limits and left adjoints preserve colimits.


Consider an adjunction as in Definition 3.3 and a limit of a diagram as in Definition 3.12. To show that the limit is preserved by the right adjoint, we must show that

defines a relative right adjoint. By Lemma 3.10, it suffices to demonstrate this after pasting with the relative right adjoint encoded by the component at of the counit of the adjunction , as below-left:

From the 2-functoriality of the exponential in a cartesian closed 2-category, and . Hence, the pasting diagram displayed above-left equals the one displayed above-center, which equals the diagram above-right. This latter diagram is a pasted composite of relative right adjoints, and is then a relative right adjoint in its own right by Lemma 3.10.

Universal properties

Definitions 3.3 and 3.12 do not express the full universal properties of adjunctions between and co/limits in -categories. These require additional structure borne by the 2-category , namely the existence of comma -categories for any pair of -functors and . The comma -category is an -category equipped with canonical functors and an -natural transformation as below-left, formed by the pullback of -categories below-right:

While the universal property of as an object of is weaker than the standard notion of comma object in 2-category theory, nevertheless:

Theorem 3.15 (RV2, 3.5.8).

An -functor admits a right adjoint relative to if and only if there exists an equivalence over :

When Theorem 3.15 is applied to and , it specializes to:

Corollary 3.16 (RV2, 4.1.1).

An -functor admits a right adjoint if and only if .

When Theorem 3.15 is applied to and it specializes to:

Corollary 3.17 (RV2, 4.3.1).

A diagram has a limit if and only if .

Here the comma -category defines the -category of cones over . The -category admits a terminal element , which defines a right adjoint to the unique functor . Via the equivalence we see that the limit cone is terminal in the -category of cones. Indeed, admits a limit if and only if the -category of cones admits a terminal element RV2, 4.3.2.

Could we teach this to undergraduates?

If classical category theory were a standard course in the undergraduate mathematics curriculum, then perhaps students with a particular interest in the subject might go on to learn some 2-category theory, like students with a particular interest in algebra might go on to take more specialized courses in classical algebraic geometry, algebraic number theory, or representation theory when offered. From this point, the proofs of the results stated here are not too difficult.

But these results encompass only a small portion of -category theory, and for most of the rest there is a greater jump in complexity when extending from 1-categories to -categories. This is best illustrated by considering the Yoneda lemma, which in an important special case is stated as follows:

Theorem 3.18 (RV2, 5.7.1).

Given an -category and elements , the -groupoid is equivalent to the -groupoid of functors over .

One direction of this equivalence is easy to describe: the map from right to left is defined by evaluation at the identity element . The inverse equivalence defines the Yoneda embedding, which is notoriously difficult to construct in -category theory as it involves equipping with a homotopy coherent composition function L2, §5.1.3.

To achieve further simplifications of -category theory, one idea is to ask our foundation system to do more of the work.

4. A Synthetic Theory of -Categories

To explain the desiderata for an alternative foundation, consider the default notions of “sameness” for -categorical data. Two elements in an -category are the same if and only if they are connected by a path in the underlying -groupoid, while parallel morphisms are the same if and only if they are connected by an invertible 2-cell, defining a path in the appropriate mapping space. For an -categorical construction to be “well-defined” it must:


respect the notions of sameness encoded by paths in suitable spaces, and


respect equivalences between these spaces themselves, since they are only well-defined as homotopy types.

Axiomatizing sameness

In traditional foundations, there is a similar axiom that mathematical constructions or results must respect sameness as encoded by equality. The axioms that define the binary relation in first-order logic are:

reflexivity: for all , is true.

indiscernibility of identicals: for all and for all predicates , if then holds if and only if holds.

Analogous rules govern Martin-Löf’s identity types in an alternative foundational framework for constructive mathematics known as dependent type theory M-L. Here the primitives include types like , , and and terms like , , , which may depend on an arbitrary context of variables drawn from previously defined types (e.g., the appearing in three examples above).⁠Footnote11 In traditional foundations, mathematical structures are defined in the language of set theory, while proofs obey the rules of first-order logic. In dependent type theory, mathematical constructions and mathematical proofs are unified: both are given by terms in appropriate types. The ambient type then describes the sort of object being constructed or the mathematical statement being proven, while the context describes the inputs to the construction or the hypotheses for the theorem.


In a mathematical statement of the form “Let …be …then …” the stuff following the “let” likely declares the names of the variables in the context described after the “be,” while the stuff after the “then” most likely describes a type or term in that context.

The rules for Martin-Löf’s identity types include:⁠Footnote12


One additional rule, not listed here, concerns the computational behavior of this system.

identity-formation: in the context of two variables there is a type .

Types encode mathematically meaningful statements or assertions, so this rule says that it is reasonable to inquire whether and might be identified, once and are terms in the same type. Certain identity types, such as , will be empty, since the terms and cannot be identified, but the type nevertheless exists.

identity-introduction: for any , there is a term .

Terms in types are witnesses to the truth of the statement encoded by the type, so this rule corresponds to the reflexivity axiom.

identity-elimination: given any family of types depending on and , to provide a family of terms for all it suffices to provide a family of terms for all .

This rule implies Leibniz’s indiscernibility of identicals and much more besides:

Theorem 4.1 (BGLu).

The iterated identity types provide any type with the structure of an -groupoid, in which the terms are the points, the identifications are the paths, and the higher identifications encode homotopies.

In low dimensions, the -groupoid structure on the iterated identity types of a type provides:

functions that invert identifications,

functions that compose identifications,

higher identifications between composable triples of identifications,

and much more. All of these terms are constructed using the identity-elimination rule from the reflexivity terms provided by the identity-introduction rule. Since an identification defines a path from to in the -groupoid , identifications in dependent type theory are often referred to colloquially as “paths.”

The homotopical interpretation of dependent type theory

The homotopical interpretation of dependent type theory was discovered in the early 21st century by Awodey–Warren and Voevodsky, building on earlier work of Hofmann and Streicher. This connection inspired Voevodsky to make the following definition:

Definition 4.2.

A type is contractible just when there is a term of type

which may be read as “there exists , so that for all , is identifiable with with all quantifiers interpreted as requiring continuous specifications of data.⁠Footnote13


The definition of contractible types makes use of the dependent pair and dependent function types in dependent type theory. A term of type provides a term , the “center of contraction,” together with a family of paths for all , the “contracting homotopy.”

Just as contractible spaces might contain uncountably infinitely many points, contractible types might contain more than one term. But since any two terms in a contractible type may be identified, and since identity-elimination implies that all of dependent type theory respects identifications, the theory behaves as if a contractible type had a unique term.

Univalent foundations

Martin-Löf’s dependent type theory is a formal system in which all constructions are continuous in paths, our first desideratum. The second desideratum, of well-definedness under equivalences between types, follows once Voevodsky’s univalence axiom is added to dependent type theory, resulting in a formal system called homotopy type theory or univalent foundations.

Voevodsky’s univalence connects two notions of sameness for types. In traditional dependent type theory, types can be encoded as terms in a universe of types.⁠Footnote14 Thus, one notion of sameness between types belonging to a universe is given by paths in the universe. Another notion of sameness is suggested by types as -groupoids: for any and there is a type of (homotopy) equivalences from to .⁠Footnote15 By identity-elimination, to define a natural map it suffices to define the image of , which we take to be the identity equivalence. The univalence axiom asserts that this map is an equivalence for all types and .


Russell’s paradox can be resolved by a cumulative hierarchy of universes.


It is an interesting challenge to define a type whose data witnesses that a given map is an equivalence in such a way that this type is contractible whenever it is inhabited.

By univalence, an equivalence gives rise to a path , which can then be used to transport terms in any type involving to terms in the corresponding type involving . Thus, univalent mathematics is automatically invariant under equivalence between types.

-categories in univalent foundations

There is an experimental exploration of -category theory RSBWBa in an extension of homotopy type theory in which every type has a family of arrows in addition to the family of paths . These types are obtained from a new type-forming operation that produces extension types, whose terms are type-valued diagrams that strictly extend a given diagram along an inclusion of “shapes” (polytopes embedded in directed cubes constructed in the theory of a strict interval) RS, §2-4. Extension types include types analogous to the pullbacks of 1.4 and 3.14.

The formal system has semantics in complete Segal spaces RSW so it provides a rigorous way to prove theorems about -categories as understood in traditional foundations. At the same time, the experience of working with -categories in this “univalent” foundational setting is much more akin to the experience of working with 1-categories in traditional foundations.

It takes work to set up this formal system and considerably more to describe its interpretation in complete Segal spaces; indeed, this is where the hard work of solving homotopy coherence problems goes. But once this is done, it is possible to define the notion of an -category, something that would no doubt be reassuring to undergraduates hoping to learn about them.⁠Footnote16 The two axioms express the “Segal” and “completeness” conditions of Rezk’s model R1, respectively.


Recall that in the formal -category theory developed in the 2-category , a concrete definition of -categories is not used.

Definition 4.3 (RS, 5.3,10.6).

An -category is a type in which:

every composable pair of arrows has a unique composite, and

for any pair of terms the natural map from paths in to isomorphisms in is an equivalence.

The “uniqueness” in the first axiom is in the sense of Definition 4.2: what it asserts is that a suitable space of composites analogous to Definition 1.3 is contractible—the default meaning of uniqueness in this formal system. Like in the space defined by 1.4, a term in the space of composites provides a higher-dimensional witness to the composition relation. A composition function

is obtained by throwing away these witnesses. Like any construction in homotopy type theory, this function respects identifications and is therefore well-defined. It follows from this axiom that composition is associative and unital, using canonical identity arrows .

The second axiom involves a type of isomorphisms in , which may be defined in a similar manner to the type of equivalences between types RS, §10.

The Yoneda lemma

The advantages of this synthetic framework for -category theory are on display when comparing the proofs of the Yoneda lemma in RV2, 5.7.1 and in RS, 9.1. We sketch the latter here in the same special case considered in Theorem 3.18.

Theorem 4.4 (RS, 9.1).

Given an -category and elements , the type is equivalent to the type of fiberwise functions.

A key difference between Theorem 3.18 and Theorem 4.4 is that in the present framework it is straightforward to define the inverse equivalence to the evaluation at identity map. The inverse equivalence takes an arrow to the natural map . The usual proof then demonstrates that these maps are inverse equivalences. In one direction, this is given by an identification , which expresses the fact that composition in an -category is unital. In the other direction, we must show that a fiberwise map agrees with the map whose component at is given by . By a consequence of the univalence axiom called “function extensionality,” it suffices to show that . This follows from the fact that fiberwise maps are automatically “natural,” providing an identification . Since the function respects the identification , we obtain the required identification.

In fact, RS, 9.5 proves a generalization of the Yoneda lemma that was first discovered with this formal system and later proven in traditional foundations RV2, 5.7.2


Significant technical problems remain to make it feasible to teach -category theory to undergraduates, but I have hope that in the future the subject will not seem as forbidding as it does today.


Tim Campion, Maru Sarazola, Mike Shulman, Dominic Verity, and Jonathan Weinberger all provided helpful suggestions on an early draft version of this article, while John Bourke suggested the rebranding of absolute lifting diagrams as relative adjunctions. Further improvements were made in response to comments from Steven Sam and three anonymous referees. The author is also grateful to receive support from the NSF via the grants DMS-1652600 and DMS-2204304, from the ARO under MURI Grant W911NF-20-1-0082, from the AFOSR under award number FA9550-21-1-0009, and from a Simons Foundation Fellowship.


C. Bardomiano Martínez, Limits and colimits of synthetic -categories, 2022, arXiv:2202.12386.
Benno van den Berg and Richard Garner, Types are weak -groupoids, Proc. Lond. Math. Soc. (3) 102 (2011), no. 2, 370–394, DOI 10.1112/plms/pdq026. MR2769118Show rawAMSref\bib{vBG}{article}{ label={BG}, author={van den Berg, Benno}, author={Garner, Richard}, title={Types are weak $\omega $-groupoids}, journal={Proc. Lond. Math. Soc. (3)}, volume={102}, date={2011}, number={2}, pages={370--394}, issn={0024-6115}, review={\MR {2769118}}, doi={10.1112/plms/pdq026}, } Close amsref.
Julia E. Bergner, The homotopy theory of -categories, London Mathematical Society Student Texts, vol. 90, Cambridge University Press, Cambridge, 2018. MR3791455Show rawAMSref\bib{Bergner:2018ht}{book}{ label={Be}, author={Bergner, Julia E.}, title={The homotopy theory of $(\infty , 1)$-categories}, series={London Mathematical Society Student Texts}, volume={90}, publisher={Cambridge University Press, Cambridge}, date={2018}, pages={xiv+273}, isbn={978-1-107-49902-7}, isbn={978-1-107-10136-4}, review={\MR {3791455}}, } Close amsref.
J. M. Boardman and R. M. Vogt, Homotopy invariant algebraic structures on topological spaces, Lecture Notes in Mathematics, Vol. 347, Springer-Verlag, Berlin-New York, 1973. MR0420609Show rawAMSref\bib{BV}{book}{ label={BV}, author={Boardman, J. M.}, author={Vogt, R. M.}, title={Homotopy invariant algebraic structures on topological spaces}, series={Lecture Notes in Mathematics, Vol. 347}, publisher={Springer-Verlag, Berlin-New York}, date={1973}, pages={x+257}, review={\MR {0420609}}, } Close amsref.
U. Buchholtz and J. Weinberger, Synthetic fibered -category theory, 2021, arXiv:2105.01724.
A. Grothendieck, Pursuing stacks, 1983, arXiv:2111.01000
A. Joyal, The theory of quasi-categories and its applications, Advanced Course on Simplicial Methods in Higher Categories, vol. 2, Centre de Recerca Matemática, 2008.
Ya. Varshavskiĭ and D. Kazhdan, The Yoneda lemma for complete Segal spaces (Russian, with Russian summary), Funktsional. Anal. i Prilozhen. 48 (2014), no. 2, 3–38, DOI 10.1007/s10688-014-0050-3; English transl., Funct. Anal. Appl. 48 (2014), no. 2, 81–106. MR3288174Show rawAMSref\bib{KV}{article}{ label={KV}, author={Varshavski\u {\i }, Ya.}, author={Kazhdan, D.}, title={The Yoneda lemma for complete Segal spaces}, language={Russian, with Russian summary}, journal={Funktsional. Anal. i Prilozhen.}, volume={48}, date={2014}, number={2}, pages={3--38}, issn={0374-1990}, translation={ journal={Funct. Anal. Appl.}, volume={48}, date={2014}, number={2}, pages={81--106}, issn={0016-2663}, }, review={\MR {3288174}}, doi={10.1007/s10688-014-0050-3}, } Close amsref.
J. Lurie, On -topoi, 2003, arXiv:0306109.
Jacob Lurie, Higher topos theory, Annals of Mathematics Studies, vol. 170, Princeton University Press, Princeton, NJ, 2009, DOI 10.1515/9781400830558. MR2522659Show rawAMSref\bib{lurie-topos}{book}{ label={L2}, author={Lurie, Jacob}, title={Higher topos theory}, series={Annals of Mathematics Studies}, volume={170}, publisher={Princeton University Press, Princeton, NJ}, date={2009}, pages={xviii+925}, isbn={978-0-691-14049-0}, isbn={0-691-14049-9}, review={\MR {2522659}}, doi={10.1515/9781400830558}, } Close amsref.
J. Lurie, Higher algebra, 2017,
Peter LeFanu Lumsdaine, Weak -categories from intensional type theory, Typed lambda calculi and applications, Lecture Notes in Comput. Sci., vol. 5608, Springer, Berlin, 2009, pp. 172–187, DOI 10.1007/978-3-642-02273-9_14. MR2550047Show rawAMSref\bib{lumsdaine}{article}{ label={Lu}, author={Lumsdaine, Peter LeFanu}, title={Weak $\omega $-categories from intensional type theory}, conference={ title={Typed lambda calculi and applications}, }, book={ series={Lecture Notes in Comput. Sci.}, volume={5608}, publisher={Springer, Berlin}, }, date={2009}, pages={172--187}, review={\MR {2550047}}, doi={10.1007/978-3-642-02273-9\_14}, } Close amsref.
Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium ’73 (Bristol, 1973), Studies in Logic and the Foundations of Mathematics, Vol. 80, North-Holland, Amsterdam, 1975, pp. 73–118. MR0387009Show rawAMSref\bib{PML}{article}{ label={M-L}, author={Martin-L\"{o}f, Per}, title={An intuitionistic theory of types: predicative part}, conference={ title={Logic Colloquium '73}, address={Bristol}, date={1973}, }, book={ series={Studies in Logic and the Foundations of Mathematics, Vol. 80}, publisher={North-Holland, Amsterdam}, }, date={1975}, pages={73--118}, review={\MR {0387009}}, } Close amsref.
Daniel G. Quillen, Homotopical algebra, Lecture Notes in Mathematics, No. 43, Springer-Verlag, Berlin-New York, 1967. MR0223432Show rawAMSref\bib{Quillen}{book}{ label={Q}, author={Quillen, Daniel G.}, title={Homotopical algebra}, series={Lecture Notes in Mathematics, No. 43}, publisher={Springer-Verlag, Berlin-New York}, date={1967}, pages={iv+156 pp. (not consecutively paged)}, review={\MR {0223432}}, } Close amsref.
Charles Rezk, A model for the homotopy theory of homotopy theory, Trans. Amer. Math. Soc. 353 (2001), no. 3, 973–1007, DOI 10.1090/S0002-9947-00-02653-2. MR1804411Show rawAMSref\bib{rezk-CSS}{article}{ label={R1}, author={Rezk, Charles}, title={A model for the homotopy theory of homotopy theory}, journal={Trans. Amer. Math. Soc.}, volume={353}, date={2001}, number={3}, pages={973--1007}, issn={0002-9947}, review={\MR {1804411}}, doi={10.1090/S0002-9947-00-02653-2}, } Close amsref.
Charles Rezk, A Cartesian presentation of weak -categories, Geom. Topol. 14 (2010), no. 1, 521–571, DOI 10.2140/gt.2010.14.521. MR2578310Show rawAMSref\bib{rezk-cartesian}{article}{ label={R2}, author={Rezk, Charles}, title={A Cartesian presentation of weak $n$-categories}, journal={Geom. Topol.}, volume={14}, date={2010}, number={1}, pages={521--571}, issn={1465-3060}, review={\MR {2578310}}, doi={10.2140/gt.2010.14.521}, } Close amsref.
Emily Riehl and Dominic Verity, Homotopy coherent adjunctions and the formal theory of monads, Adv. Math. 286 (2016), 802–888, DOI 10.1016/j.aim.2015.09.011. MR3415698Show rawAMSref\bib{RV-adj}{article}{ label={RV1}, author={Riehl, Emily}, author={Verity, Dominic}, title={Homotopy coherent adjunctions and the formal theory of monads}, journal={Adv. Math.}, volume={286}, date={2016}, pages={802--888}, issn={0001-8708}, review={\MR {3415698}}, doi={10.1016/j.aim.2015.09.011}, } Close amsref.
Emily Riehl and Dominic Verity, Elements of -category theory, Cambridge Studies in Advanced Mathematics, vol. 194, Cambridge University Press, Cambridge, 2022, DOI 10.1017/9781108936880. MR4354541Show rawAMSref\bib{RV}{book}{ label={RV2}, author={Riehl, Emily}, author={Verity, Dominic}, title={Elements of $\infty $-category theory}, series={Cambridge Studies in Advanced Mathematics}, volume={194}, publisher={Cambridge University Press, Cambridge}, date={2022}, pages={xix+759}, isbn={978-1-108-83798-9}, review={\MR {4354541}}, doi={10.1017/9781108936880}, } Close amsref.
Emily Riehl and Michael Shulman, A type theory for synthetic -categories, High. Struct. 1 (2017), no. 1, 147–224, DOI 10.1007/s42001-017-0005-6. MR3912054Show rawAMSref\bib{RS}{article}{ label={RS}, author={Riehl, Emily}, author={Shulman, Michael}, title={A type theory for synthetic $\infty $-categories}, journal={High. Struct.}, volume={1}, date={2017}, number={1}, pages={147--224}, review={\MR {3912054}}, doi={10.1007/s42001-017-0005-6}, } Close amsref.
J. Weinberger, Strict stability of extension types, 2022, arXiv:2203.07194.


Opening image is courtesy of nevarpp via Getty.

Photo of Emily Riehl is courtesy of Marshall Clarke.