nLab universal fibration of (infinity,1)-categories




The universal fibration of (∞,1)-categories is the generalized universal bundle of (,1)(\infty,1)-categories in that it is Cartesian fibration

p:Z(,1)Cat op p \colon Z \to (\infty,1)Cat^{op}

over the opposite category of the (∞,1)-category of (∞,1)-categories such that

  • its fiber p 1(C)p^{-1}(C) over C(,1)CatC \in (\infty,1)Cat is just the (,1)(\infty,1)-category CC itself;

  • every Cartesian fibration p:CDp : C \to D arises as the pullback of the universal fibration along an (∞,1)-functor S p:D(,1)Cat opS_p : D \to (\infty,1)Cat^{op}.

Recall from the discussion at generalized universal bundle and at stuff, structure, property that for n-categories at least for low nn the corresponding universal object was the nn-category nCat *n Cat_* of pointed nn-categories. ZZ should at least morally be (,1)Cat *(\infty,1)Cat_*.


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

One description of the universal cartesian fibration is given in section 3.3.2 of HTT as the contravariant (∞,1)-Grothendieck construction applied to the identity functor ((,1)Cat op) op(,1)Cat((\infty,1)Cat^{op})^{op} \to (\infty,1)Cat.

We can also give a more direct description:


Z opZ^{op} is equivalent to the full subcategory of (,1)Cat [1](\infty,1)Cat^{[1]} spanned by the morphisms of the form [C x/C][C_{x/} \to C] for small (∞,1)-categories CC and objects xCx \in C.

The universal fibration Z(,1)Cat opZ \to (\infty,1)Cat^{op} is opposite to the target evaluation.

Dually, the universal cocartesian fibration is Z(,1)CatZ' \to (\infty,1)Cat where ZZ' is the (∞,1)-category of arrows of the form [C /xC][C_{/x} \to C].


This is the proof idea of this mathoverflow post.

By proposition of Higher Topos Theory, there are presentable fibrations RFib(,1)CatRFib \to (\infty,1)Cat and (,1)Cat [1]tgt(,1)Cat(\infty,1)Cat^{[1]} \xrightarrow{tgt} (\infty,1)Cat classifying functors C𝒫(C)C \mapsto \mathcal{P}(C) and C(,1)Cat /CC \mapsto (\infty,1)Cat_{/C}.

By proposition of Higher Topos Theory, the yoneda embedding j:C𝒫(C)j : C \to \mathcal{P}(C) is a natural transformation, and the covariant Grothendieck construction provides a cocartesian functor ZRFibZ' \to RFib. Since it is fiberwise fully faithful and () !(-)_! preserves representable presheaves, we can identify ZZ' with the full subcategory of RFibRFib consisting of the representable presheaves.

The Grothendieck construction provides a fully faithful 𝒫(C)(,1)Cat /C\mathcal{P}(C) \to (\infty,1)Cat_{/C} whose essential image is the right fibrations. The contravariant Grothendieck construction a cartesian functor RFib(,1)Cat [1]RFib \to (\infty,1)Cat^{[1]}. Since it is fiberwise fully faithful and pullbacks preserve right fibrations, we can identify RFibRFib with the full subcategory of (,1)Cat [1]( \infty,1)Cat^{[1]} spanned by right fibrations.

By the relationship between the covariant and contravariant Grothendieck constructions, the universal cartesian fibration is classified by op:((,1)Cat op) op(,1)Catop : ((\infty,1)Cat^{op})^{op} \to (\infty,1)Cat.


A key point of this description is that for any small (∞,1)-category CC, the functor xC /xx \mapsto C_{/x} (where xyx \to y acts by composition) is a fully faithful functor C(,1)Cat /CC \to (\infty,1)Cat_{/C}. Dually, xC x/x \mapsto C_{x/} is a fully faithful functor C op(,1)Cat /CC^{op} \to (\infty,1)Cat_{/C}

The hom-spaces of the universal cocartesian fibration can be described as

Z([C /xC],[D /yD])Core(eval xy) Z'([C_{/x} \to C], [D_{/y} \to D]) \simeq Core(eval_x \downarrow y)

where eval x:D CDeval_x : D^C \to D. This should be compared with the lax slice 2-category construction. In fact, ZZ' can be constructed by taking the underlying (∞,1) category of the lax coslice (or colax, depending on convention) over the point of the (∞,2)-category of (∞,1)-categories.

For \infty-Groupoids


The universal fibration of (,1)(\infty,1)-categories restricts to a Cartesian fibration Z| GrpdGrpd opZ|_{\infty Grpd} \to \infty Grpd^{op} over ∞Grpd by pullback along the inclusion morphism Grpd(,1)Cat\infty Grpd \hookrightarrow (\infty,1)Cat

Z| Grpd Z Grpd op (,1)Cat op. \array{ Z|_{\infty Grpd} &\longrightarrow& Z \\ \big\downarrow && \big\downarrow \\ \infty Grpd^{op} &\hookrightarrow& (\infty,1)Cat^{op} } \,.

The ∞-functor Z| GrpdGrpd opZ|_{\infty Grpd} \to \infty Grpd^{op} is even a right fibration and it is the universal right fibration. In fact it is (when restricted to small objects) the object classifier in the (∞,1)-topos ∞Grpd, see at object classifier – In ∞Grpd.


The universal left fibration is the forgetful functor Grpd *Grpd\infty Grpd_* \to \infty Grpd. Its opposite is the universal right fibration.

(Lurie 2009, Prop,, Cisinski 2019, Sec. 5.2, for the further restriction to the universal Kan fibration see also Kapulkin & Lumsdaine 2021)


The following are equivalent:


This is proposition in HTT.


For concretely constructing the relation between Cartesian fibrations p:ECp : E \to C of (∞,1)-categories and (∞,1)-functors F p:C(,1)CatF_p : C \to (\infty,1)Cat one may use a Quillen equivalence between suitable model categories of marked simplicial sets.

For CC an (∞,1)-category regarded as a quasi-category (i.e. as a simplicial set with certain properties), the two model categories in question are

The Quillen equivalence between these is established by the relative nerve? construction

N (C):[C,SSet]SSet/C. N_{-}(C) : [C,SSet] \to SSet/C \,.

By the adjoint functor theorem this functor has a left adjoint

F (C):SSet/C[C,SSet]. F_{-}(C) : SSet/C \to [C,SSet] \,.

For p:ECp : E \to C a left Kan fibration the functor F p(C):CSSetF_p(C) : C \to SSet sends cObj(C)c \in Obj(C) to the fiber p 1(c):=E× C{c}p^{-1}(c) := E \times_C \{c\}

F p(C):cp 1(c). F_p(C) : c \mapsto p^{-1}(c) \,.

(See remark of HTT).


Textbook accounts:

The direct description of the universal fibration is discussed at

Discussion of the universal Kan fibration as a categorical semantics for a univalent type universe in homotopy type theory:

Discussion of fibrations via (∞,2)-category theory

On the categorical semantics of homotopy type theory in simplicial sets/ \infty -groupoids:

Discussion of straightening and unstraightening entirely within the context of quasi-categories:

which (along the lines of the discussion of the universal left fibration from Cisinski 2019) allows to understand the universal coCartesian fibration as categorical semantics for the univalent type universe in directed homotopy type theory:

(see video 3 at 1:16:58 and slide 3.33).

Last revised on March 29, 2023 at 16:20:43. See the history of this page for a list of all contributions to it.