category object in an (infinity,1)-category


Internal (,1)(\infty,1)-Categories

(,1)(\infty,1)-Category theory

(,1)(\infty,1)-Topos Theory

(∞,1)-topos theory





Extra stuff, structure and property



structures in a cohesive (∞,1)-topos



The notion of (∞,1)-category may be formulated internal to any other (,1)(\infty,1)-category with sufficient properties (with a rich enough internal logic). This generalizes the notion of internal category from category theory to (∞,1)-category theory. In fact, an internal category in an (,1)(\infty,1)-category is automatically, externally, itself an (∞,1)-category.

A category internal to some given (,1)(\infty,1)-category 𝒞\mathcal{C} is a simplicial object in an (∞,1)-category A:Δ op𝒞A : \Delta^{op} \to \mathcal{C} in 𝒞\mathcal{C}, where the object in degree kk is to be thought of as “the object of kk-tuples of composable morphisms” in AA. This is formalized by requiring the canonical morphisms A kA 1× A 0× A 0A 1A_k \to A_1 \times_{A_0} \cdots \times_{A_0} A_1 (into the iterated (∞,1)-pullback over the source and target maps) to be an equivalence in 𝒞\mathcal{C} (the “Segal condition”).

If 𝒞\mathcal{C} happens to be just a 1-category, then this already makes AA an internal category. Generally, however, 𝒞\mathcal{C} comes with its own notion of homotopy, and one must ask in addition that the notion of equivalence in AA is compatible with that in 𝒞\mathcal{C} (the “completeness condition”).

A general abstract way of formalizing this is given in Lurie, sections 1.1, 1.2. For historical reasons, the notion of internal (,1)(\infty,1)-category there goes by the name complete Segal space object, in honor of the notion of a complete Segal space (due to Charles Rezk and in turn chosen in honor of the Segal conditions for ordinary categories), which is an internal (,1)(\infty,1)-category in 𝒞=\mathcal{C} = ∞Grpd. But more generally we can consider internal category in a more general (∞,1)-topos, and these are (∞,2)-sheaves of (∞,1)-categories

There are a variety of model category structures that present the (,1)(\infty,1)-category of all internal (,1)(\infty,1)-categories in a suitable 𝒞\mathcal{C}, which typically go as models for complete Segal space objects. The soundness of these models is discussed below in Model category presentations (Lurie, section 1.5).

Motivation and introduction

Before coming to the formal definitions below in Definition, here are some words for the reader looking for introduction and orientation into the general problem of formulating categories internally in homotopy theory.

Whatever exactly the right or desired nature of a category internal to an (,1)(\infty,1)-category/homotopy theory is (and we will see that there are some subtleties to beware of and some variants to account for), the bare minimum must be that it consists of

  1. a collection X 0X_0 of objects – but we shouldn’t say set of objects, of course, instead the generic terminology is: a type of objects and so we should write

    X 0:Type\vdash \; X_0 \colon Type;

  2. for each pair x 0,x 1:X 0x_0, x_1 \colon X_0 of objects, an (x 0,x 1)(x_0,x_1)-dependent type of morphisms X 1(x 0,x 1)X_1(x_0,x_1) “from x 0x_0 to x 1x_1,

    x 0,x 1:X 0X 1(x 0,x 1)x_0, x_1 \colon X_0 \;\vdash \; X_1(x_0, x_1).

(One might decide to collect these all together to a single type X 1x 0,x 1:TypeX 1(x 0,x 1)X_1 \coloneqq \underset{x_0,x_1 \colon Type}{\sum} X_1(x_0,x_1), but the theory flows much more naturally if we do keep the dependency on the objects explicit.)

At this point one might be tempted to proceed in close analogy to traditional formulations in internal category theory in non-homotopic 1-category theory and consider an explicit composition function

x 0,x 1,x 2:X 0comp x 0,x 1,x 2:X 1(x 0,x 1)×X 1(x 1,x 2)X 1(x 0,x 2) x_0, x_1, x_2 \colon X_0 \;\vdash\; comp_{x_0,x_1,x_2} \colon X_1(x_0,x_1) \times X_1(x_1, x_2) \to X_1(x_0, x_2)

to be thought of as taking a pair (g,f)(g,f) of composable morphisms to their composite morphism gfg \circ f, and demand that it satisfies associativity up to homotopy. This approach is explored below in the section H-category types, where it is also discussed that this is not the correct notion of category objects internal to a homotopy-theoretic context.

To get a hint for what the correct formulation should be, it is useful to turn this around and investigate which internal-homotopy-theory structure an ordinary small category (internal to Set) gives rise to.

Namely, bare homotopy theory is about groupoids and then n-groupoids and ∞-groupoids, and so it should be relevant that a groupoid is itself a category and that, conversely, every category CCat(Set)C \in Cat(Set) already contains some “homotopy theory”, namely its maximal groupoid, its core i C:core(C)Ci_C \colon core(C) \to C. This groupoid is “the homotopy theory of the objects of CC” in the sense that is contains all the information about the objects and their equivalences. Therefore it is natural to regard this as the “type of objects” and declare X 0core(C)X_0 \coloneqq core(C), regarded as an object of objects in the ambient (∞,1)-category Grpd \hookrightarrow ∞Grpd.

But once we take that perspective, it is clear what the type X 1X_1 of morphisms should be: it should be the comma object of the core inclusion with itself: X 1(i C/i C)X_1 \coloneqq (i_C/i_C).

This is exposition is further developed in Segal space – construction from a category. There it is discussed how proceeding this way, one finds from CC a homotopy-theoretic kind of nerve which is now not a simplicial object in Set anymore (a simplicial set) as the nerve in ordinary category theory is, but which is now a simplicial object in an (∞,1)-category, namely in Grpd \hookrightarrow ∞Grpd. In degree kk \in \mathbb{N} it contains not the set of sequences of composable morphisms, but the “space” of such sequences, which just as the “space” X 0X_0 of objects knows all the homotopies, namely all the equivalences between such sequences of composable morphisms.

One then recalls a basic fact of traditional category theory: a simplicial set is the nerve of a category precisely if it satisfies the Segal conditions: which say that it is built from certain iterated fiber products of the 1-simplices over the vertices. Accordingly, here one should expect that the simplicial groupoid X X_\bullet is built in degree kk by a kk-fold homotopy fiber product of the space of 1-simplices over the space of vertices, and indeed one finds that it is.

In traditional category theory a simplicial set is the nerve of a category if and only if it satisfies the Segal conditions. Does the converse already hold here? The above inspection shows that instead of the core inclusion i C:core(C)Ci_C \colon core(C) \to C we could have started with any functor i:KCi \colon K \to C and X ni / nX_n \coloneqq i^{/^n} would still defined a simplicial groupoid that satisfies the Segal conditions. So in homotopy theory the Segal conditions, which witness the fact that we formed a nerve by iterated homotopy fiber product, need to be accompanied by one more condition which ensures that we are indeed forming the homotopy fiber product not of any map, but of the core-inclusion (this is often, but somewhat undescrptively, called the “compleness condition”, and more recently also called a univalence condition).

Finally, the nerve of a category in fact contains lots of redundant information. It is 2-coskeletal and hence in a precise sense already its 2-skeleton X 2X 1X 0X_2 \stackrel{\to}{\stackrel{\to}{\to}} X_1 \stackrel{\to}{\to} X_0 contains all the relevant information. Therefore we may decide to write this out explicitly in terms of a further dependent type X 2X_2 of compositions. This explicit 2-skeletal formulation of internal (1,1)-categories in homotopy theory is spelled out below in (1,1)-Category types.

But of course the point of category objects internal ot an (,1)(\infty,1)-category is to speak about structures of higher homotopical degree, hence about untruncated simplicial objects in an (∞,1)-category and the appropriate conditions on them to qualify as internal categories. The comprehensive discussion of this definition we turn to in Definition.


We define category objects internal to an (∞,1)-category 𝒞\mathcal{C} (and with respect to a choice of “inclusion of groupoids” H𝒞\mathbf{H}\hookrightarrow \mathcal{C}) by a sequence of full (co)reflective sub-(∞,1)-categories

HCat H(𝒞)PreCat H(𝒞)𝒞 Δ op \mathbf{H} \hookrightarrow Cat_{\mathbf{H}}(\mathcal{C}) \hookrightarrow PreCat_{\mathbf{H}}(\mathcal{C}) \hookrightarrow \mathcal{C}^{\Delta^{op}}

of that of

The definition makes recourse to the notion of groupoid object in an (∞,1)-category, and so we first review that in

Then we discuss the definition of

The canonical example here is the archtypical (∞,1)-topos H=\mathbf{H} = ∞Grpd of ∞-groupoids: a category object internal to that is essentially what is also called a complete Segal space. But the definition works for any other (∞,1)-topos, hence for general (∞,1)-categories of (∞,1)-sheaves (of ∞-stacks).

More generally, given a fully faithful inclusion H𝒞\mathbf{H} \hookrightarrow \mathcal{C} of an (∞,1)-topos into some other (∞,1)-category, we can define

The archetypical example here is the case where again H=\mathbf{H} = ∞Grpd =:(,0)Cat=: (\infty,0)Cat and where then, by induction on nn, the inclusion is Grpd(,n)Cat\infty Grpd \hookrightarrow (\infty,n)Cat that of \infty-groupoids into (∞,n)-categories. The resulting internal category objects are then externally essentially (n+1)-fold complete Segal spaces, hence (,n+1)(\infty,n+1)-categories.

But again, more generally, H\mathbf{H} can be an (∞,1)-category of (∞,1)-sheaves and 𝒞\mathcal{C} for instance an (∞,2)-topos of (∞,2)-sheaves, yielding (,3)(\infty,3)-sheaves, and so on.

Simplicial objects

Let 𝒞\mathcal{C} be an (∞,1)-category. We discuss in the following a sequence of reflective sub-(∞,1)-categories of that of simplicial objects in an (∞,1)-category 𝒞 Δ op\mathcal{C}^{\Delta^{op}} in 𝒞\mathcal{C}, see there for more details.

We frequently refer to the powering of a simplicial object X X_\bullet by a simplicial set, into an object in 𝒞\mathcal{C}, denoted X(K)X(K). For details on this see at simplicial object in an (∞,1)-category – Powering .


It is noteworthy that category objects internal to 𝒞\mathcal{C}, as defined below, will form a full sub-(∞,1)-category of that of simplicial objects in an (∞,1)-category. In traditional theory of internal categoriesa major issue is that in general there are not enough internal functors: the full subcategory of internal graphs on the internal categories needs to be further localized, in general. But this turns out to be an artefact of the ambient category being an (n,1)-category for nn too low.

For a discussion of how for plain internal categories (those that also externally are 1-categories) the traditional localization becomes superfluous if the ambient context is a (2,1)-category (instead of just a 1-category) see at 2-topos the section In terms of internal categories. The following may be thought of as a generalization of that discussion.

Pre-category objects

Let 𝒞\mathcal{C} be an (∞,1)-category with finite (∞,1)-limits


An internal precategory XX in 𝒞\mathcal{C} is a simplicial object in an (∞,1)-category

X:Δ op𝒞 X : \Delta^{op} \to \mathcal{C}

such that it satifies the Segal condition, hence such that for all nn \in \mathbb{N}, XX exhibits X([n])X([n]) as the (∞,1)-limit / iterated (∞,1)-pullback

X([n])X({0,1})×X([0])×X[0]X({n1,n}) nfactors. X([n]) \simeq \underbrace{ X(\{0,1\}) \underset{X([0])}{\times} \cdots \underset{X[0]}{\times} X(\{n-1,n\}) }_{n \; factors} \,.

Write PreCat(𝒞)PreCat(\mathcal{C}) for the (,1)(\infty,1)-category of internal pre-categories in 𝒞\mathcal{C}, the full sub-(∞,1)-category of the simplicial objects on the internal precategories.

This is called a category object in (Lurie, def. 1.1.1). Here we reserve that term for those objects that behave more like category objects should, which are the complete Segal space objects, below.


By the discussion at Segal conditions – In terms of sheaf conditions, this means that PreCat(𝒞)PreCat(\mathcal{C}) sits in an (∞,1)-pullback square in (∞,1)Cat

PreCat(𝒞) 𝒞 Δ op Graphs(𝒞) 𝒞 Δ 0 op, \array{ PreCat(\mathcal{C}) &\hookrightarrow& \mathcal{C}^{\Delta^{op}} \\ \downarrow && \downarrow \\ Graphs(\mathcal{C}) &\hookrightarrow& \mathcal{C}^{\Delta_0^{op}} } \,,

where Δ 0 opΔ\Delta_0^{op} \to \Delta is the wide subcategory of the simplex category on the injective maps that moreover send elementary edges to elementary edges (morphisms of linear graphs), and the bottom morphism is the functor that sends a graph object X 1 0 1X 0X_1 \stackrel{\overset{\partial_1}{\to}}{\underset{\partial_0}{\to}} X_0 to the object which in degree nn is X 1×X 0×X 0X 1 nfactors\underbrace{ X_1 \underset{X_0}{\times} \cdots \underset{X_0}{\times} X_1}_{n\; factors}.


The Segal conditions imply that for X X_\bullet a pre-category object, there is a composition map

X 1× X 0X 1( 0, 2) 1X 2 1X 1 X_1 \times_{X_0} X_1 \underoverset{\simeq}{(\partial_0, \partial_2)^{-1}}{\to} X_2 \stackrel{\partial_1}{\to} X_1

which satisfies associativity and the unit law up to higher coherent homotopy. A subobject in an (∞,1)-category YX 1Y \hookrightarrow X_1 on such that restricted along this inclusion this composition becomes invertible we call a subobject of equivalences.


For X X_\bullet a pre-category object, def. 7, write

Equiv(X 1)X 1 Equiv(X_1) \hookrightarrow X_1

for the maximal subobject in an (∞,1)-category of the object of 1-morphisms on those which are equivalences with respect to the composition of remark 3.

Groupoid objects

A groupoid object is a pre-category object, def. 7 whose composition operation according to remark 3 is invertible. This is discussed in more detail at groupoid object in an (∞,1)-category. Here we briefly recall the

and then discuss the crucial property for the further developments here, which is the


Let 𝒞\mathcal{C} be an (∞,1)-category with finite (,1)(\infty,1)-limits.


A groupoid object in 𝒞\mathcal{C} is a simplicial object in an (∞,1)-category

X:Δ op𝒞 X : \Delta^{op} \to \mathcal{C}

satisfying the following equivalent conditions

  1. X X_\bullet satisfies the groupoidal Segal conditions, meaning that for all nn \in \mathbb{N} and all partitions [n]SS[n] \simeq S \cup S' that share a single element SS={s}S \cap S' = \{s\}, the (∞,1)-functor XX exhibits an (∞,1)-pullback

    X([n])X(S)× X(SS)X(S); X([n]) \simeq X(S) \times_{X(S \cap S')} X(S') \,;
  2. X X_\bullet is a pre-category object, def. 7, and the morphism

    X(Δ 2)X(Λ 0 2) X(\Delta^2) \to X(\Lambda^2_0)

    is an equivalence in 𝒞\mathcal{C}.

Write Grpd(𝒞)Grpd(\mathcal{C}) for the (∞,1)-category of groupoid objects in 𝒞\mathcal{C}, the full sub-(∞,1)-category of simplicial objects on the groupoid objects.

The equivalence follows with HTT prop., see at groupoid object – equivalent characterizations.


For 𝒞=Grpd\mathcal{C} = \infty Grpd, a groupoid object XX in 𝒞\mathcal{C} is a pre-category object X PreCat(𝒞)𝒞 Δ opX_\bullet \in PreCat(\mathcal{C}) \hookrightarrow \mathcal{C}^{\Delta^{op}}, def. 7, such that the full inclusion

Equiv(X 1)X 1 Equiv(X_1) \hookrightarrow X_1

is an equivalence in an (∞,1)-category.


We are to think of X([0])X([0]) as the 𝒞\mathcal{C}-object of objects of a groupoid internal to 𝒞\mathcal{C}, and of X([1])X([1]) as its 𝒞\mathcal{C}-object of morphisms. In terms of this the above condition says two things:

  1. for SSS \cup S' an order-preserving partition (meaning that for all sSs \in S, sSs' \in S' we have sss \leq s') it says that X([n])X([n]) may be identified with the object of sequences of lenght nn of composable morphisms;

  2. for SSS \cup S' not order-preserving, it says that morphisms have inverses. For instance for the partition of [2][2] given by S={0,1}S = \{0,1\} and S={0,2}S' = \{0,2\} the above says intuitively that diagrams in the internal groupoid of the form

    b a c \array{ && b \\ & \nearrow && \searrow \\ a &&&& c }

    (an inner horn) are equivalent to those of the form

    b a c \array{ && b \\ & \nearrow && \\ a &&\to&& c }

    (an outer horn).

    The equivalence defines and is defined by forming the inverse of the morphism bcb \to c.

Accordingly, below a category object is defined analogously, but demanding the above condition only for ordered decompositions.

There will be one additional condition on category objects (“completeness”). In order to see where this comes from, notice the following.


There is a full and faithful (∞,1)-functor

const:𝒞Grpd(𝒞) const : \mathcal{C} \hookrightarrow Grpd(\mathcal{C})

sending an object XX of 𝒞\mathcal{C} to the corresponding constant simplicial object (constX):[n]X(const X) : [n] \mapsto X.

If 𝒞\mathcal{C} has small (∞,1)-colimits, then this is a reflective embedding, whose reflector

lim :Grpd(𝒞)𝒞 \lim_\to : Grpd(\mathcal{C}) \to \mathcal{C}

forms the (∞,1)-colimit in 𝒞\mathcal{C} over the simplicial diagram underlying a groupoid object.

See (Lurie, example 1.1.4).

Coreflection into pre-category objects

In order to state the completeness condition on a precategory object, def. 7, we need to reflect, or rather coreflect, it onto its core groupoid object, def. 3.

We first consider this for the ambient (∞,1)-topos H\mathbf{H} being ∞Grpd, then we use that to deal with the general case.


For X Grpd Δ opX_\bullet \in \infty Grpd^{\Delta^{op}} a precategory object, def. 7, its corresponding H-category is, up to equivalence, the Ho(∞Grpd)-enriched category hX h X_\bullet with

  • the objects are the points of X 0X_0 (more invariantly: the objects are any set of points in X 0X_0 containing at least one point in each connected components);

  • the homotopy type of morphisms for any pair (x 0,x 1)(x_0,x_1) of objects is that of the of the (∞,1)-pullback

    hX(x 0,X1){x 0}×X 0X 1×X 0{x 1}GrpdHo(Grpd) h X(x_0,X1) \coloneqq \{x_0\} \underset{X_0}{\times} X_1 \underset{X_0}{\times} \{x_1\} \in \infty Grpd \to Ho(\infty Grpd)
  • the composition comp x 0,x 1,x 2comp_{x_0,x_1, x_2} is given by the morphism

    hX(x 0,x 1)×hX(x 1,x 2) {x 0}×X 0{x 1}×X 0X 1×X 0{x 2} {x 0}×X 0X 1×X 0X 1×X 0{x 2} {x 0}×X 0X 2×X 0{x 1} 1{x 0}×X 0X 1×X 0{x 2} =hX(x 0,x 2), \begin{aligned} h X(x_0,x_1) \times h X(x_1, x_2) & \simeq \{x_0\} \underset{X_0}{\times} \{x_1\} \underset{X_0}{\times} X_1 \underset{X_0}{\times} \{x_2\} \\ & \to \{x_0\} \underset{X_0}{\times} X_1 \underset{X_0}{\times} X_1 \underset{X_0}{\times} \{x_2\} \\ & \stackrel{\simeq}{\to} \{x_0\} \underset{X_0}{\times} X_2 \underset{X_0}{\times} \{x_1\} \\ & \stackrel{\partial_1}{\to} \{x_0\} \underset{X_0}{\times} X_1 \underset{X_0}{\times} \{x_2\} \\ & = h X(x_0,x_2) \end{aligned} \,,

where the second map is an isomorphism in Ho(∞Grpd) which is the inverse of the equivalence in ∞Grpd that exists by the Segal conditions assumed to be satisfied by X X_\bullet.

(In (Lurie) this is def. 1.1.6.)


For X Grpd Δ opX_\bullet \in \infty Grpd^{\Delta^{op}} a pre-category object, we say that a point f:*X 1f \colon * \to X_1 in the degree-1 object is an equivalence if it is an isomorphism in the category hXh X, def. 4. For nn \in \mathbb{N}, n1n \geq 1, write

Equiv(X n)X n Equiv(X_n) \hookrightarrow X_n

for the 1-monomorphism that includes the full-sub-\infty-groupoid on the sequences of equivalences. Write furthermore

Core(X) Grpd(Grpd)Grpd Δ op Core(X)_\bullet \in Grpd(\infty Grpd) \hookrightarrow \infty Grpd^{\Delta^{op}}

for the simplicial object with

Core(X) 0X 0 Core(X)_0 \coloneqq X_0


Core(X) nEquiv(X n). Core(X)_n \coloneqq Equiv(X_n) \,.

This is evidently a groupoid object, def. 3, called the core of the pre-category object X X_\bullet.


This is a more abstract formulation of what equivalently is presented by the corresponding discussion for Segal spaces and complete Segal space, see at complete Segal space – Definition.

In order to state the completeness condition on pre-category objects that make them be genuine category objects, we need this core-construction exhibits groupoid objects as a coreflective sub-(∞,1)-category of pre-category objects.


Let H\mathbf{H} be an (∞,1)-topos. Every groupoid object in H\mathbf{H} is canonically an internal pre-category. Under this inclusion i:Grpd(H)PreCat(H)i \colon Grpd(\mathbf{H}) \hookrightarrow PreCat(\mathbf{H}) the groupoid objects form a coreflective sub-(∞,1)-category of that of pre-catgegory objects,

(icore):Grpd(H)CorePreCat(H). (i \dashv core) \colon Grpd(\mathbf{H}) \stackrel{\hookrightarrow}{\underset{Core}{\leftarrow}} PreCat(\mathbf{H}) \,.

The coreflection is the core operation that discards non-invertible morphisms.

This is (Lurie, prop. 1.1.14).


With def. 5 it is direct to establish the statement for the case that 𝒞\mathcal{C} \simeq ∞Grpd, (Lurie, cor. 1.1.11), for instance by using the standard theory of Segal spaces. From this it follows also for the case that HPSh (𝒟)\mathbf{H} \simeq PSh_\infty(\mathcal{D}) is an (∞,1)-category of (∞,1)-presheaves by arguing objectwise over objects in 𝒟\mathcal{D}. In the general case, H\mathbf{H} is a reflective sub-(∞,1)-category of such, 𝒞PSh (𝒟)\mathcal{C} \hookrightarrow PSh_\infty(\mathcal{D}). It is then sufficient to show that the core operation on the presheaf \infty-toposes respects these inclusions, so that we have

Grpd(H) Grpd(PSh (𝒟)) Core Core PSh PreCat(H) PreCat(PSh (𝒟)). \array{ Grpd(\mathbf{H}) &\hookrightarrow& Grpd(PSh_\infty(\mathcal{D})) \\ \downarrow \uparrow^{\mathrlap{Core}} && \downarrow \uparrow^{\mathrlap{Core}_{PSh}} \\ PreCat(\mathbf{H}) &\hookrightarrow& PreCat(PSh_\infty(\mathcal{D})) } \,.

This means that we need to show that if X X_\bullet is degreewise in HPSh (𝒟)\mathbf{H} \hookrightarrow PSh_\infty(\mathcal{D}) and is a pre-category object, then Core PSh(X )Core_{PSh}(X_\bullet) is degreewise in H\mathbf{H}. By the pre-category condition and since the refletive inclusion is right adjoint and hence preserves the fiber products, for this it is sufficient that Core Psh(X) 0Core_{Psh}(X)_0 and Core PSh(X) 1Core_{PSh}(X)_1 are in H\mathbf{H}. To complete the proof it is sufficient to show that the first of these is X 0X_0 and (again since the inclusion preserves limits) the second is equivalent to the powering X(K)X(K), where

KΔ 0 Δ {0,2}Δ 3 Δ {1,3}Δ sSet K \coloneqq \Delta^0 \coprod_{\Delta^{\{0,2\}}} \Delta^3 \coprod_{\Delta^{\{1,3\}}} \Delta^ \;\;\; \in sSet

is the simplicial set obtained from the 3-simplex by collapsing the (0,2)(0,2)-edge and the {1,3}\{1,3\}-edge. Write K 0{1,2}KK^0 \coloneqq \{1,2\} \hookrightarrow K for the image of the (1,2)(1,2)-edge of Δ 3\Delta^3. Schematically:

K={1 K 0 0 id 0 11 K 0 0 id 0 1}. K = \left\{ \array{ 1 &\stackrel{K^0}{\to}& 0 \\ \uparrow &\nearrow_{\mathrlap{id}}& \downarrow \\ 0 &\to& 1 } \;\;\; \Rightarrow \;\;\; \array{ 1 &\stackrel{K^0}{\to}& 0 \\ \uparrow &\searrow^{\mathrlap{id}}& \downarrow \\ 0 &\to& 1 } \right\} \,.

We claim generally that

  1. for XPreCat(H)X \in PreCat(\mathbf{H}) the canonical morphism Core(X)(K)X(K)Core(X)(K) \to X(K) is an equivalence;

  2. for YGrpd(H)Y \in Grpd(\mathbf{H}) the canonical morphism Y(K)Y(K 0)Y(K) \to Y(K^0) is an equivalence.

(This is (Lurie, prop. 1.1.13).)


X(K)X 0×X({0,2})X 3×X({1,3})X 0 X(K) \simeq X_0 \underset{X(\{0,2\})}{\times} X_3 \underset{X(\{1,3\})}{\times} X_0

etc. By construction, Core(X)(K)X(K)Core(X)(K) \to X(K) is fully faithful. Hence to see that it is an equivalence, hence in addition essentially surjective, it is sufficient to observe that

X(K)X 0×X {0,1}X 3×X {1,3}X 0 X(K) \simeq X_0 \underset{X_{\{0,1\}}}{\times} X_3 \underset{X_{\{1,3\}}}{\times} X_0

is the space of those 3-simplices in X X_\bullet for which the {0,1}\{0,1\}-edges is a weak inverse to the {2,3}\{2,3\}-edge. Hence Core(X)(K)X(K)Core(X)(K) \to X(K) is an equivalence. Moreover K 0KK^0 \hookrightarrow K is a weak equivalence, and hence so is Core(X)(K)Core(X)(K 0)Core(X) 1Core(X)(K) \to Core(X)({K^0}) \simeq Core(X)_1, by this proposition at simplicial object in an (∞,1)-category.

Category objects

In an (,1)(\infty,1)-topos

Let H\mathbf{H} be an (∞,1)-topos. Then every object of H\mathbf{H} may already be thought of as being an internal groupoid, which facilitates the definition of internal categories. This we discus here. The more general case where the ambient (,1)(\infty,1)-category is not necessarily an (∞,1)-topos is discussed further below.


An internal category in an (∞,1)-topos H\mathbf{H} is an internal pre-category X H Δ opX_\bullet \in \mathbf{H}^{\Delta^{op}}, def. 7, such that its core Core(X)Core(X) is in the image of the inclusion const:HGrpd(H)const \colon \mathbf{H} \hookrightarrow Grpd(\mathbf{H}) of prop. 1.

This is called a complete Segal space object in (Lurie, def. 1.2.10).


A groupoid object, def. 3, is always a pre-category object, but is a category object only and precisely if it is in the image of the constant inclusion Const:HGrpd(H)Const \colon \mathbf{H} \to Grpd(\mathbf{H}).

In a sense these are the genuine groupoid objects, while the others are groupoid objects equipped with an atlas (…).

For internalizing in an (,1)(\infty,1)-category 𝒞\mathcal{C} which is not an (∞,1)-topos, we need to specify what the constant groupoid objects in 𝒞\mathcal{C} are supposed to be. This is the topic of

Once one has this, the definition of

works essentially as before in an (,1)(\infty,1)-topos. The key point is that the ambient (∞,1)-topos H\mathbf{H} serves itself naturally as the collection of groupoid objects inside its (∞,1)-category of inernal categories and so this yields a natural notion of

Internal to the archetypical base (,1)(\infty,1)-topos ∞Grpd these are, externally, the bare (∞,n)-categories. Internal to an (∞,1)-category of (∞,1)-sheaves over some (∞,1)-site, these are the (∞,n+1)-sheaves on that site. More on this is in the


Relative core – Choice of groupoid objects

The structure necessary to formulate the completeness condition, which in an (∞,1)-topos is def. 5, internal to a more general (∞,1)-category 𝒞\mathcal{C} is the following.


For 𝒞\mathcal{C} an presentable (∞,1)-category, a choice of internal groupoids is a choice of full sub-(∞,1)-category inclusion H𝒞\mathbf{H} \hookrightarrow \mathcal{C} of an (∞,1)-topos H\mathbf{H} such that

This is the definition of “distributor” in (Lurie, def. 1.2.1), where we are making use of (Lurie, remark 1.2.6) which identifies H\mathbf{H} here as being necessarily an (∞,1)-topos, by the (∞,1)-Giraud theorem.


The identity H𝒞\mathbf{H} \simeq \mathcal{C} is a choice of internal groupoids in H\mathbf{H}, by the (∞,1)-Giraud theorem. For this choice the following theory of category objects in 𝒞\mathcal{C} relative to H\mathbf{H} reduces to that of category objects in H\mathbf{H}, as discussed above.

For the discussion of (∞,n)-categories, the central property of such choices of internal groupoids, def. 6 is that they behave well with forming internal categories, this is cor. 2 below.

This corresponds to (Lurie, notation 1.2.9).

In a general (,1)(\infty,1)-category

In the following, let 𝒞\mathcal{C} be a presentable (∞,1)-category eqipped with a choice of internal groupoids H𝒞\mathbf{H} \hookrightarrow \mathcal{C}, def. 6.


An internal precategory XX in 𝒞\mathcal{C} relative to the choice of internal groupoids H𝒞\mathbf{H} \hookrightarrow \mathcal{C} is a simplicial object

X:Δ op𝒞 X : \Delta^{op} \to \mathcal{C}

such that

  1. for all nn \in \mathbb{N} the functor XX exhibits X nX_n as the (∞,1)-limit / iterated (∞,1)-pullback
X([n])X({0,1})× X([0])× X[0]X({n1,n}) X([n]) \simeq X(\{0,1\}) \times_{X([0])} \cdots \times_{X[0]} X(\{n-1,n\})
  1. such that the object of objects lies in the inclusion of H\mathbf{H}

    X 0H𝒞.X_0 \in \mathbf{H} \hookrightarrow \mathcal{C}\,.

Write PreCat H(𝒞)PreCat_{\mathbf{H}}(\mathcal{C}) for the (,1)(\infty,1)-category of internal pre-categories in 𝒞\mathcal{C} relative to H\mathbf{H}, the full sub-(∞,1)-category of the simplicial objects on the internal precategories.

This is the definition of Segal object in (Lurie, def. 1.2.7).


The inclusion

Grpd(H)PreCat(H)PreCat H(𝒞) Grpd(\mathbf{H}) \hookrightarrow PreCat(\mathbf{H}) \hookrightarrow PreCat_{\mathbf{H}}(\mathcal{C})

has a right adjoint (∞,1)-functor

Core H:PreCat H(𝒞)Grpd(H). Core_{\mathbf{H}} : PreCat_{\mathbf{H}}(\mathcal{C}) \to Grpd(\mathbf{H}) \,.

The left morphism has a right adjoint by prop. 2. The right adjoint of the right functor is implied by the first of the axioms on the choice of groupoids Disc:H𝒞Disc \colon \mathbf{H} \hookrightarrow \mathcal{C}, by which DiscDisc has a right adjoint Γ\Gamma and is itself a right adjoint. This means that their prolongations to simplicial objects both preserve pre-category objects and hence induce an adjunction of pre-category objects. Moreover, since DiscDisc is in addition fully faithful, Γ\Gamma takes objects in the inclusion back to themselves, and hence this preserves also (H𝒞)(\mathbf{H}\hookrightarrow \mathcal{C})-relative precategory objects.


An internal pre-category X 𝒞 Δ opX_\bullet \mathcal{C}^{\Delta^{op}}, def. 7, is called an internal category if its H\mathbf{H}-Core, def. 3, is an essentially constant groupoid object, hence if

Core H(A)HconstGrpd(H). Core_{\mathbf{H}}(A) \in \mathbf{H} \stackrel{const}{\hookrightarrow} Grpd(\mathbf{H}) \,.


Cat H(𝒞)PreCat H(𝒞) Cat_{\mathbf{H}}(\mathcal{C}) \hookrightarrow PreCat_{\mathbf{H}}(\mathcal{C})

for the full sub-(∞,1)-category of internal precategories on the internal categories.

This is (Lurie, def. 1.2.10).


The inclusion of pre-category objects, def. 7 into category objects is reflective

Cat H(𝒞)LPreCat H(𝒞). Cat_{\mathbf{H}}(\mathcal{C}) \stackrel{\overset{L}{\leftarrow}}{\hookrightarrow} PreCat_{\mathbf{H}}(\mathcal{C}) \,.

This is (Lurie, remark 1.2.11).


By prop. 1 and by the first axiom in def. 6, we have a reflective inclusion

HconstH Δ opDisc Δ op𝒞 Δ op. \mathbf{H} \stackrel{const}{\hookrightarrow} \mathbf{H}^{\Delta^{op}} \stackrel{Disc^{\Delta^{op}}}{\hookrightarrow} \mathcal{C}^{\Delta^{op}} \,.

From this the right adjoint core, prop. 3, induces the claimed inclusion by using the statement of reflective sub-(∞,1)-category – Transport of reflective subategories, which says that Cat H(𝒞)Core 1(H)(PreCat H(𝒞))Cat_{\mathbf{H}}(\mathcal{C}) \simeq Core^{-1}(\mathbf{H})(PreCat_{\mathbf{H}}(\mathcal{C})) is a reflective inclusion

H const 𝒞 Δ op Core incl Core incl Cat H(𝒞) PreCat H(𝒞). \array{ \mathbf{H} &\stackrel{const}{\hookrightarrow}& \mathcal{C}^{\Delta^{op}} \\ {}^{\mathllap{Core}}\uparrow\downarrow^{\mathrlap{incl}} && {}^{\mathllap{Core}}\uparrow\downarrow^{\mathrlap{incl}} \\ Cat_{\mathbf{H}}(\mathcal{C}) &\hookrightarrow& PreCat_{\mathbf{H}}(\mathcal{C}) } \,.

In summary we have:


In summary we have a reflective inclusion

Cat HPreCat H(𝒞)𝒞 Δ op. Cat_{\mathbf{H}} \hookrightarrow PreCat_{\mathbf{H}}(\mathcal{C}) \hookrightarrow \mathcal{C}^{\Delta^{op}} \,.

So far we have only ever used the first axiom in def. 6. We now describe the reflector PreCat H(𝒞)Cat H(𝒞)PreCat_{\mathbf{H}}(\mathcal{C}) \to Cat_{\mathbf{H}}(\mathcal{C}) in more detail, and for that we use the other two axioms.

The corresponding reflector is “Segal completion”. We now describe this in more detail.


For X ,Y PreCat (𝒞)X_\bullet, Y_\bullet \in PreCat_{\mathcal{H}}(\mathcal{C}), a morphism f :X Y f_\bullet \colon X_\bullet \to Y_\bullet of pre-category objects (hence of the underlying simplicial objects) is a categorical equivalence if

  1. essential surjectivitylim(core(X ))lim(core(Y ))\underset{\to}{\lim}(core(X_\bullet)) \to \underset{\to}{\lim} (core(Y_\bullet)) is an equivalence in H\mathbf{H};

  2. full faithfulness – the diagram

    X 1 f 1 Y 1 ( 0, 1) ( 0, 1) X 0×X 0 (f 0,f 0) Y 0×Y 0 \array{ X_1 &\stackrel{f_1}{\to}& Y_1 \\ \downarrow^{\mathrlap{(\partial_0,\partial_1)}} && \downarrow^{\mathrlap{(\partial_0,\partial_1)}} \\ X_0 \times X_0 &\stackrel{(f_0,f_0)}{\to}& Y_0 \times Y_0 }

    is an (∞,1)-pullback diagram in 𝒞\mathcal{C}.


The inclusion Cat H(𝒞)PreCat H(𝒞)Cat_{\mathbf{H}}(\mathcal{C}) \hookrightarrow PreCat_{\mathbf{H}}(\mathcal{C}) of def. 7 is reflective. The reflector

L:PreCat H(𝒞)Cat H(𝒞) L \colon PreCat_{\mathbf{H}}(\mathcal{C}) \to Cat_{\mathbf{H}}(\mathcal{C})

inverts precisely the categorical equivalences, def. 8.

This is (Lurie, theorem 1.2.13).


In particular, by reflectivity, this means that a morphism f :X Y f_\bullet \colon X_\bullet \to Y_\bullet in Cat H(𝒞)Cat_\mathbf{H}(\mathcal{C}) is an equivalence (hence an equivalence in 𝒞 Δ op\mathcal{C}^{\Delta^{op}}) precisely if it is a categorical equivalence.

Iterated internalization – Internal nn-categories

A central point of the formulation of internal category objects is that it can be iterated to yields categories objects internal to category objects … internal to an (,1)(\infty,1)-topos.


Let H𝒞\mathbf{H} \hookrightarrow \mathcal{C} be a choice of internal groupoids, def. 6. Then also the constant inclusion

HCat H(𝒞) \mathbf{H} \hookrightarrow Cat_{\mathbf{H}}(\mathcal{C})

into the (,1)(\infty,1)-category of the corresponding category objects is a choice of internal groupoids.

This is (Lurie, prop.1.3.2).


We consider the first of the three axioms, that the inclusion preserves limits and colimits: The constant inclusion

HconstH Δ opDisc Δ op𝒞 Δ op \mathbf{H} \stackrel{const}{\to} \mathbf{H}^{\Delta^{op}} \stackrel{Disc^{\Delta^{op}}}{\to} \mathcal{C}^{\Delta^{op}}

is fully faithful, since Δ op\Delta^{op} is a contractible (,1)(\infty,1)-category . The first inclusion preserves limits and colimits since in presheaf categories these are computed objectwise, similarly for the second, using the condition that already Disc:H𝒞Disc \colon \mathbf{H} \to \mathcal{C} preserves limits and colimits. Moreover, this inclusion clearly factors through Cat H(𝒞)𝒞 Δ opCat_{\mathbf{H}}(\mathcal{C}) \hookrightarrow \mathcal{C}^{\Delta^{op}}, by def. 7, and since that is also fully faithful, also HCat H(𝒞)\mathbf{H} \to Cat_{\mathbf{H}}(\mathcal{C}) preserves limits and colimits.

In particular therefore we have the following:


For H\mathbf{H} an (∞,1)-topos, the canonical inclusion

HconstGrpd(H)Cat(H) \mathbf{H} \stackrel{const}{\hookrightarrow} Grpd(\mathbf{H}) \hookrightarrow Cat(\mathbf{H})

is a choice of internal groupoids in Cat(H)Cat(\mathbf{H}), in the sense of def. 6. Moreover, by induction, each of the induced constant inclusions

HconstCat(Cat((Cat(H)))) \mathbf{H} \stackrel{const}{\hookrightarrow} Cat(Cat(\cdots (Cat(\mathbf{H}))))

is a choice of internal groupoids.

This is (Lurie, corollary 1.3.4, variant 1.3.8).

Therefore it makes sense to write:


Let H\mathbf{H} be an (∞,1)-topos. For n=0n = 0 set

0Cat(H)H. 0 Cat(\mathbf{H}) \coloneqq \mathbf{H} \,.

Then by induction on nn \in \mathbb{N} set

(n+1)Cat(H)Cat H(nCat(H)). (n+1)Cat(\mathbf{H}) \coloneqq Cat_{\mathbf{H}}(n Cat(\mathbf{H})) \,.

We call nCat(H)n Cat(\mathbf{H}) the (,1)(\infty,1)-category of (∞,n)-categories in H\mathbf{H}, or of (∞,n+1)-sheaves or (-stacks) of (,n)(\infty,n)-categories on (the (∞,1)-site of definition of) H\mathbf{H}.

See also at n-category object in an (∞,1)-category.

Enriched categories as internal categories

The 1-categorical notion of enriched category is similar to that of internal category, a main difference being that an internal category has an object of objects in the ambient category 𝒞\mathcal{C}, whereas an enriched category has a set/class of objects. If, however, 𝒞\mathcal{C} is equipped with a notion of discrete objects, thought of as the inclusion of sets into 𝒞\mathcal{C}, then 𝒞\mathcal{C}-enriched categories may be thought of as those categories internal to 𝒞\mathcal{C} such that their object of objects is discrete.

Accordingly, if for 𝒞\mathcal{C} a presentable (∞,1)-category equipped with a choice of internal groupoids H𝒞\mathbf{H} \hookrightarrow \mathcal{C}, def. 6, for H\mathbf{H} \simeq ∞Grpd, then an ACat H(𝒞)A \in Cat_{\mathbf{H}}(\mathcal{C}) by definition has a bare (external / discrete) \infty-groupoid “of objects”. The underlying simplicial object is thus more like a Segal category object (though still different from that).

In (Lurie, def. 1.3.3) such an choice of internal groupoids Grpd𝒞\infty Grpd \hookrightarrow \mathcal{C} is called an “absolute distributor”.


For 𝒞=H\mathcal{C} = \mathbf{H} an (∞,1)-topos over ∞Grpd, the inverse image of its global section geometric morphism GrpdH\infty Grpd \to \mathbf{H} is a choice of internal groupoids, def. 6, precisely if H\mathbf{H} is locally and globally ∞-connected.

(ΠDiscΓ):HΓDiscΠGrpd (\Pi \dashv \Disc \dashv \Gamma) : \mathbf{H} \stackrel{\stackrel{\Pi}{\to}}{\stackrel{\overset{Disc}{\hookleftarrow}}{\underset{\Gamma}{\to}}} \infty Grpd


Model category presentations

We discuss here presentations of category objects internal to an (,1)(\infty,1)-category by model category theory methods.


Let CC be a left proper combinatorial model category that presents the (∞,1)-category 𝒞\mathcal{C} in that 𝒞C \mathcal{C} \simeq C^\circ.

Then the category [Δ op,C][\Delta^{op}, C] of simplicial objects in CC admits a left proper combinatorial model category structure characterized by the following properties:

  1. it is a left Bousfield localization of the injective or projective or Reedy model structure on functors [Δ op,C] proj/inj/Reedy[\Delta^{op}, C]_{proj/inj/Reedy};

  2. an object Δ opC\Delta^{op} \to C is fibrant precisely if it is fibrant in [Δ op,C] proj/inj/Reedy[\Delta^{op}, C]_{proj/inj/Reedy} and if the corresponding simplicial object Δ opC \Delta^{op}\to C^\circ in the (∞,1)-category presented by CC is an internal category.

This is stated as (Lurie, prop. 1.5.4).


By the discussion at model structure on functors. Either of [Δ op,C] proj/inj/Reedy[\Delta^{op}, C]_{proj/inj/Reedy} is a presentation of 𝒞 op\mathcal{C}^{op}; and moreover, by the discussion at reflective sub-(∞,1)-category – model category presentation the reflective inclusion Cat H(𝒞)𝒞 Δ opCat_{\mathbf{H}}(\mathcal{C}) \hookrightarrow \mathcal{C}^{\Delta^{op}} of cor. 1 is presented by the left Bousfield localization as claimed.


For C=sSet QuillenC = sSet_{Quillen} the standard model structure on simplicial sets, this gives in particular rise to the standard model structure for complete Segal spaces.

Homotopy type theory formulation

For H\mathbf{H} an (∞,1)-topos, another way of saying that we have an internal category object in H\mathbf{H} should be to say that we formulate it in the internal language of H\mathbf{H}, which is a homotopy type theory.

However, at the time of this writing little is known for how to speak of non-finite diagrams fully internally. To appreciate the issue, notice that the “internal” formulation of categories by simplicial objects in an (∞,1)-category as above is in fact not fully internal to the ambient (,1)(\infty,1)-category 𝒞\mathcal{C}, but assumes that it is known what externally an (∞,1)-functor Δ op𝒞\Delta^{op} \to \mathcal{C} is. When we speak in homotopy type theory this is not an option and we have to genuinely stick to internal reasoning.

Nevertheless, we can speak fully internally of (,n)(\infty,n)-categories for “low nn” by making use of the following observations.

  1. By the discussion at semi-Segal space a category object should equivalently be a semi-category object X X_\bullet: a semi-simplicial object satisfying the Segal conditions, and which is unital in that Eq(X 1)X 1 1X 0Eq(X_1) \hookrightarrow X_1 \stackrel{\partial_1}{\to} X_0 is an equivalence.

    A similar formalization of 1-category objects in homotopy type theory has been presented and studied in some detail in (AKS).

  2. To finite (and “low”) degree a semi-simplicial type may be given “by hand” as a sequence of dependent types like this:

    X 0:Type x 0,x 1:X 0 X 1(x 0,x 1):Type x 0,x 1,x 2:X 1;f 2:X 1(x 0,x 1);f 1:X 1(x 0,x 2);f 2:X 1(x 0,x 1) X 2(f 0,f 1,f 2):Type \begin{aligned} & \vdash\; X_0 \colon Type \\ x_0,x_1 \colon X_0 \;& \vdash \; X_1(x_0,x_1) \colon Type \\ x_0,x_1,x_2 \colon X_1; f_2 \colon X_1(x_0,x_1); f_1 \colon X_1(x_0,x_2); f_2 \colon X_1(x_0,x_1) \; & \vdash \; X_2(f_0,f_1,f_2) \colon Type \\ \vdots \; &\vdash\; \vdots \end{aligned}

    etc. (Where in principle we can go on like this to any finite nn; but it is open how to say this in one go for all nn at once.)

    Notice that in the model-categorical semantics of dependent types in homotopy type theory, such a structure interprets indeed (up to the given degree) as a Reedy fibrant semi-simplicial object as used in the standard model-category theoretic constructions of internal \infty-categories discussed above.

  3. If X 0X_0 is n-truncated (h-level n+2n+2) so that we are dealing with an internal category that is externally an (n,1)-category, then a complete semi-Segal object X X_\bullet should indeed already be determined by its simplicial skeleton X 0n+2X_{0 \leq \bullet \leq n+2}.

So in conclusion an nn-truncated category type in homotopy type theory should be an (n+2)(n+2)-skeleton of a semi-simplicial type X 03X_{0 \leq \bullet \leq 3} as above, such that

  1. Segal condition: for each 2kn2 \leq k \leq n the canonical function X nX 1× X 0× X 0X 1X_n \to X_1 \times_{X_0} \cdots \times_{X_0} X_1 into the nn-fold homotopy pullback is an equivalence;

  2. univalence/unitality: the canonical function Eq(X 1)X 1 1X 0Eq(X_1) \to X_1 \stackrel{\partial_1}{\to} X_0 is an equivalence.

  3. X 0X_0 is n-truncated (of h-level n+2n+2).

We spell this out in more detail below for


(homotopy coherence by dependent types)

The formulation of simplicial objects in an (∞,1)-category in the internal language of homotopy type theory has to deal with the issue of formulating a simplicial “homotopy coherent diagram” in the internal language. One may think of the above formulation via semisimplicial dependent types as dealing with this by

  1. discarding the explicit discussion of the degeneracy maps (which are not homotopy-theoretically necessary anyway);

  2. formulating simplicial identities not as propositional equalities (i.e. as terms of some identity type ( j i j i1)(\partial_j \circ\partial_i \simeq \partial_j \circ \partial_{i-1}) which would need to be subjected to their own coherent identities) but in fact as typing judgements: the face maps are given directly by substitution of variables on which the types of cells depend.

This is how the above formulation implicitly deals with homotopy coherence. Under categorical semantics this state of affairs translates into the statement that Reedy fibrant semisimplicial objects are already a good (fibrant+cofibrant) model for homotopy types.

H-Category types

It may be instructive to begin by discussing a notion of internal category in homotopy theory which is not an category object in an (,1)(\infty,1)-category and which does not interpret as an (∞,1)-category, but which serves to illustrate a subtlety in the correct definition. In fact, it is an internal formulation of the H-category that underlies in particular any genuine precategory object, by def. 4 above.

Notice that historically one says that:


An H-monoid is a monoid object internal to the homotopy category Ho(∞Grpd)/Ho(Top).


This means that an H-monoid is

  1. a homotopy type XX;

  2. equipped with a binary operation :X×XX\cdot \colon X \times X \to X;

  3. and equipped with a point i:*Xi \colon * \to X

such that

  1. there exists an associativity homotopy

    (()(()()))((()())()):X×X×XX \left(\left(-\right) \cdot \left(\left(-\right) \cdot \left(-\right)\right)\right) \Rightarrow \left(\left(\left(-\right) \cdot \left(-\right)\right) \cdot \left(-\right)\right) \colon X \times X \times X \to X
  2. there exists a unitality homotopy

    (i())id:XX. (i \cdot (-)) \to id \colon X \to X \,.

The point here is that these homotopies are only required to exist, but are not specified and are not part of the data of an H-monoid.

One also speaks of an H-group for an H-monoid for which the product operation similarly has inverses up to unspecified homotopies. Hence it makes sense to consider the following many-object version (“oidification”) of this classical concept:


An H-category type XX is a

  1. a type X 0:\vdash \; X_0 \colon Type

  2. a dependent type x 0,x 1:X 0X 1(x 0,x 1):Typex_0,x_1 \colon X_0 \;\vdash\; X_1(x_0,x_1) \colon Type

  3. a term i:X 0\vdash \; i \colon X_0;

  4. a function

    x 0,x 1,x 2:X 0comp x 1,x 2,x 2:X 1(x 0,x 1)×X 1(x 1,x 2)X 1(x 0,x 2) x_0,x_1,x_2 \colon X_0 \;\vdash\; comp_{x_1,x_2,x_2} \colon X_1(x_0,x_1) \times X_1(x_1,x_2) \to X_1(x_0,x_2)

such that there is a term of identity type

x 0,x 1,x 2,x 3:X 0(com x 0,x 2,x 3comp x 0,x 1,x 2comp x 0,x 1,x 2comp x 1,x 2,x 3) x_0, x_1, x_2, x_3 \colon X_0 \;\vdash\; ( com_{x_0,x_2,x_3} \circ comp_{x_0,x_1,x_2} \simeq comp_{x_0, x_1, x_2} \circ comp_{x_1,x_2,x_3})

(hence, equivalently, a necessarily unique term of the proposition type isInhabited(…) of this identity type ).

The archetypical example of H-groups already illustrates the deficiency of this notion


For :*Y \colon * \to Y a pointed homotopy type, its loop spaceobject Ω yY\Omega_y Y is naturally equipped with the structure of an H-group by

  1. taking the unit *Ω yY* \to \Omega_y Y to be the constant loop on YY;

  2. taking the product to be given by any choice of concatenation of loops.

The natural question arising then is: how are those H-groups characterized that arise as loop space objects, this way?

One observes that those that areise this way carry much more structure than just a composition and unit up to unspecified homotopy: we can instead make an explicit choice of such homotopies by choosing ways to reparameterize the interval and, crucially, any two such choices are themselves related by a choice of higher order homotopy, and so ever on. Such a structure is called a strong homotopy monoid structure with strong homotopy associativity (as opposed to just bare homotopy associativity as in an H-monoid). Later this was abbreviated to A-∞ structure.

The classical result by Jim Stasheff answered the question by saying that:


An H-group (X,)(X, \cdot) arises as a loop space object, XΩYX \simeq \Omega Y precisely if its homotopy-monoidal structure may be lifted to an A-∞ algebra structure.

The point of the following constructions is to take care of that additional strong homotopy information.

(0,1)(0,1)-Category types

We spell out the above strategy for defining (n,1)-category types in homotopy type theory for the case of (0,1)-categories.

The following is experimental.

A (0,1)(0,1)-category type is

  1. a type X 0:Type\vdash\; X_0 \colon Type

  2. a dependent type x 0,x 1:X 0X 1(x 0,x 1):Typex_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type;

    we write

    X Δ 2x 0,x 1,x 2:X 0X 1(x 1,x 2)×X 1(x 0,x 2)×X 1(x 0,x 1); X^{\partial \Delta^2} \coloneqq \underset{x_0,x_1,x_2 \colon X_0}{\sum} X_1(x_1,x_2) \times X_1(x_0,x_2) \times X_1(x_0,x_1) \,;
  3. a dependent type

    ((x 0,x 1,x 2),(f 0,f 1,f 2)):X Δ 2X 2(f 0,f 1,f 2):Type; ((x_0,x_1,x_2), (f_0, f_1, f_2)) \colon X^{\partial \Delta^2} \;\vdash \; X_2(f_0,f_1,f_2) \colon Type \,;

such that

  1. 0-truncationX 0X_0 is 0-truncated/is an h-set

  2. 1-coskeletalness – the function

    p 1:(x 0,x 1):X 0×X 0X 1(x 0,x 1)X 0×X 0 p_1 \colon \underset{(x_0,x_1) \colon X_0 \times X_0 }{\sum} X_1(x_0,x_1) \to X_0 \times X_0

    is a 1-monomorphism;

  3. Segal condition – the function

    ((f 12,f 02,f 01)(f 12,f 01)):((x 0,x 1,x 2),(f 12,f 02,f 01)):X Δ 2X 2(x 0,x 1,x 2):X 0X 1(x 0,x 1)×X 1(x 1,x 2) ( (f_{12},f_{02},f_{01}) \mapsto (f_{12},f_{01}) ) \colon \underset{((x_0,x_1,x_2),(f_{12},f_{02},f_{01})) \colon X^{\partial \Delta^2}}{\sum} X_2 \to \underset{ (x_0,x_1,x_2) \colon X_0 }{\sum} X_1(x_0,x_1) \times X_1(x_1, x_2)

    is an equivalence;

  4. unitality – the function

    p 1:x:X 0X 1(x,x)X 0 p_1 \colon \underset{x \colon X_0}{\sum} X_1(x,x) \to X_0

    is an equivalence.

(1,1)(1,1)-Category types

We spell out the above strategy for defining (n,1)-category types in homotopy type theory for the case of (1,1)-categories.

The following is experimental.

A (1,1)(1,1)-category type is

  1. a type X 0:Type\vdash\; X_0 \colon Type

  2. a dependent type x 0,x 1:X 0X 1(x 0,x 1):Typex_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type;

    we write

    X Δ 2x 0,x 1,x 2:X 0X 1(x 1,x 2)×X 1(x 0,x 2)×X 1(x 0,x 1); X^{\partial \Delta^2} \coloneqq \underset{x_0,x_1,x_2 \colon X_0}{\sum} X_1(x_1,x_2) \times X_1(x_0,x_2) \times X_1(x_0,x_1) \,;
  3. a dependent type

    ((x 0,x 1,x 2),(f 12,f 02,f 01)):X Δ 2X 2(f 12,f 02,f 01):Type; ((x_0,x_1,x_2), (f_{12}, f_{02}, f_{01})) \colon X^{\partial \Delta^2} \;\vdash \; X_2(f_{12}, f_{02}, f_{01}) \colon Type \,;

    we write

    X Δ 3(x 0,x 1,x 2,x 3,x 4:X 1)f ij:X 1(x i,x j)X 2(f 12,f 02,f 01)×X 2(f 23,f 13,f 12)×, X^{\partial \Delta^3} \coloneqq \underset{(x_0,x_1,x_2,x_3,x_4 \colon X_1) }{\sum} \underset{ f_{i j} \colon X_1(x_i, x_j)}{\sum} X_2(f_{12},f_{02},f_{01}) \times X_2(f_{23}, f_{13}, f_{12}) \times \cdots \,,
  • a dependent type

    (σ 123,σ 023,σ 013,σ 012):X Δ 3X 3(σ 123,σ 023,σ 013,σ 012):Type (\sigma_{123}, \sigma_{023}, \sigma_{013}, \sigma_{012}) \colon X^{\partial \Delta^3} \;\vdash\; X_3(\sigma_{123}, \sigma_{023}, \sigma_{013}, \sigma_{012}) \colon Type

such that

  1. 1-truncationX 1X_1 is 1-truncated/is an h-groupoid

  2. 2-coskeletalness – the function

    p 1:(f 12,f 02,f 01):X Δ 2X 2(f 12,f 02,f 01)X Δ 2 p_1 \colon \underset{(f_{12},f_{02}, f_{01}) \colon X^{\partial \Delta^2}}{\sum} X_2(f_{12},f_{02}, f_{01}) \to X^{\partial \Delta^2}

    is a 1-monomorphism;

  3. Segal condition – the functions

    ((f 12,f 02,f 01)(f 12,f 01)):((x 0,x 1,x 2),(f 0,f 1,f 2)):X Δ 2X 2(x 0,x 1,x 2):X 0X 1(x 1,x 2)×X 1(x 0,x 1) ( (f_{12},f_{02},f_{01}) \mapsto (f_{12},f_{01}) ) \colon \underset{((x_0,x_1,x_2),(f_0,f_1,f_2)) \colon X^{\partial \Delta^2}}{\sum} X_2 \to \underset{ (x_0,x_1,x_2) \colon X_0 }{\sum} X_1(x_1,x_2) \times X_1(x_0, x_1)


    ((f ij,σ ijk)(f 01,f 12,f 23)):f ij:X 1(x i,x j)σ i 0i 1i 2:X 2(f i 1i 2,f i 0i 2,f i 0i 1)X 3(σ ,)(x 0,x 1,x 2,x 3):X 0X 1(x 0,x 1)×X 1(x 1,x 2)×X 1(x 2,x 3) ( (f_{i j}, \sigma_{i j k}) \mapsto (f_{01}, f_{12}, f_{23}) ) \colon \underset{f_{i j} \colon X_1(x_i,x_j)}{\sum} \underset{\sigma_{i_0 i_1 i_2} \colon X_2(f_{i_1 i_2}, f_{i_0 i_2}, f_{i_0 i_1})}{\sum} X_3( \sigma_{\cdots}, \cdots ) \to \underset{(x_0,x_1,x_2,x_3) \colon X_0}{\sum} X_1(x_0,x_1) \times X_1(x_1,x_2) \times X_1(x_2,x_3)

    are equivalences;

  4. unitality – the function

    (((x 0,x 1),f)x 0):x 0,x 1:X 0X 1(x 0,x 1) X 0 (((x_0,x_1),f) \mapsto x_0) \colon \underset{x_0,x_1 \colon X_0}{\sum} X_1(x_0,x_1)_{\simeq} \to X_0

    is an equivalence.


We discuss some examples and applications of the above notions. For more on examples internal to Grpd\infty Grpd see also at Segal space – examples.

The relative contexts


The canonical inclusion ∞Grpd \hookrightarrow (∞,1)Cat is a consistent “choice of groupoid objects”(“distributor”) in the sense of def. \ref{ChoiceOfGroupoidObjects}.

This is (Lurie, theorem 1.4.1).

Ordinary (,1)(\infty,1)-categories


An ordinary (∞,1)-category is equivalently an internal category in the (∞,1)-topos 𝒞:=\mathcal{C} := ∞Grpd:

Cat (,1)Cat(Grpd). Cat_{(\infty,1)} \simeq Cat(\infty Grpd) \,.

This is (Lurie, corollary 4.3.16).

Internal to ∞Grpd

The model category presentations for Cat(Grpd)Cat(\infty Grpd) discussed above are given in this case by the model structure for complete Segal spaces.


By iterating the construction of category objects, one obtains n-category objects. Externally these are (∞,n)-categories.

An ∞-groupoid may be thought of as an (∞,0)-category. Write therefore

Cat (,0):=Grpd. Cat_{(\infty,0)} := \infty Grpd \,.

Then by the above the (∞,1)-category of (∞,1)-categories is

Cat (,1)Cat(Cat (,0)). Cat_{(\infty,1)} \simeq Cat(Cat_{(\infty,0)}) \,.

Now by prop. 10 the inclusion GrpdCat(Grpd)\infty Grpd \hookrightarrow Cat(\infty Grpd) is a consistent choice of groupoid objects, and so we can continue the internalization.

Then the (,1)(\infty,1)-category Cat(𝒞)Cat(\mathcal{C}) of internal categories in 𝒞\mathcal{C} is, up to equivalence, the (,1)(\infty,1)-category of (∞,2)-categories

Cat(Cat(Grpd))Cat(Cat(Cat (,0)))Cat(Cat (,1))Cat (,2). Cat(Cat(\infty Grpd)) \simeq Cat(Cat(Cat_{(\infty,0)})) \simeq Cat(Cat_{(\infty,1)}) \simeq Cat_{(\infty,2)} \,.

This yields, with def. 9, an inductive construction of (∞,n)Cat, the (∞,1)-category of (∞,n)-categories

Cat(Cat((Cat (,0))))Cat (,n). Cat(Cat(\cdots (Cat_{(\infty,0)}))) \simeq Cat_{(\infty,n)} \,.

The corresponding model category presentation is that of n-fold complete Segal spaces.

The internal self-reflection / internal base (,1)(\infty,1)-topos

For H\mathbf{H} an (∞,1)-topos it should come canonically equipped (for each choice of regular cardinal κ\kappa) with an internal category object 𝒯𝓎𝓅ℯCat(H)\mathcal{Type} \in Cat(\mathbf{H}), which is the canonical internal base (∞,1)-topos, classifying the (relatively κ\kappa-compact part of) the codomain fibration-(∞,2)-sheaf on H\mathbf{H}.

In the syntax of homotopy type theory as discussed above the corresponding simplicial object should be

𝒯𝓎𝓅ℯ 2 [(f,g,h): (A,B,C):Type κ×Type κ×Type κ(AB)×(BC)×(AC) (gf=h):Type κ] 𝒯𝓎𝓅ℯ 1 [(A,B):Type κ AB:Type κ] 𝒯𝓎𝓅ℯ 0 [ Type κ:Type λ], \array{ \vdots && \vdots & \vdots \\ \downarrow \downarrow \downarrow \downarrow \\ \mathcal{Type}_2 & \coloneqq & [ (f,g,h) : \sum_{(A,B,C) : Type_\kappa \times Type_\kappa \times Type_\kappa} (A \to B)\times (B \to C) \times (A \to C) & \dashv (g\circ f = h) : Type_\kappa ] \\ \downarrow \downarrow \downarrow \\ \mathcal{Type}_1 & \coloneqq & [ (A,B) : Type_{\kappa} & \vdash A \to B : Type_\kappa ] \\ \downarrow \downarrow \\ \mathcal{Type}_0 & \coloneqq & [ & \vdash Type_{\kappa} : Type_\lambda] } \,,

where λ>κ\lambda \gt \kappa is another regular cardinal and where Type κType_\kappa and Type λType_\lambda are the corresponding object classifiers of the (,1)(\infty,1)-topos H\mathbf{H};

and equipped with the evident degeneracy maps

A:Types 0A(AA) A : Type \vdash s_0 A \to (A \to A)

etc. In the categorical semantics in a type-theoretic model category this makes a fibrant and cofibrant Reedy diagram, it manifestly satisfies the Segal conditions, and it is precisely univalence in the type theory that makes this a complete Segal space object.



A general abstract formulation is in

The model given by complete Segal space objects is due to

  • Charles Rezk, A model for the homotopy theory of homotopy theory. Transactions of the American Mathematical Society 35 (2001), no. 3, 973-1007

and has since seen a multitude of further developments.

Influential but unpublished discussion of higher Segal spaces is due to Clark Barwick.

Formalization in homotopy type theory

A formalization of internal 1-categories and 1-category theory in homotopy type theory is discussed in

Revised on September 27, 2013 12:44:52 by Urs Schreiber (