nLab straightening functor


This is a subentry of (∞,1)-Grothendieck construction.



When (∞,1)-categories are modeled as quasi-categories, the (∞,1)-Grothendieck construction takes the form of a Quillen equivalence between a model structure on sSet-enriched presheaves and a slice model structure of simplicial sets which has been introduced under the name straightening and unstraightening in Lurie 2009, Sec. 3.2:

Concretely, in the notation recalled at relation between quasi-categories and simplicial categories:

For a simplicial set SS, simplicially enriched category CC, and sSet-enriched functor [S]C\mathfrak{C}[S] \to C, there is a pair of adjoint functors

(St ϕUn ϕ):sSet/SSt[C op,sSet] (St_\phi\dashv Un_\phi) \;\colon\; sSet/S \xrightarrow{\;\; St \;\;} [C^{op}, sSet]

which (under an assumption on the parameter ϕ\phi) can be shown to be a Quillen equivalence between

  1. the slice category of sSet equipped with the model structure for right fibrations (also called contravariant model structure in HTT)

  2. the category of simplicial presheaves equipped with global projective model structure.

There is also a Quillen equivalence

(St ϕUn ϕ):sSet +/SSt[C op,sSet +] (St_\phi \dashv Un_\phi) \;\colon\; sSet^+/S \stackrel{St}{\;\; \longrightarrow \;\;} [C^{op}, sSet^+]


  1. the model structure for Cartesian fibrations

  2. the global projective model structure on functors with values in the model structure on marked simplicial sets.

In both cases,

  • St ϕSt_\phi is called the straightening functor

  • Un ϕUn_\phi is called the unstraightening functor.

These names have been chosen due to the fact that objects in the left hand category are defined by existential assertions and choices where on the right side these properties become coherence laws being part of the structure.


The original result is due to:

Further discussion:

Discussion internal to any (∞,1)-topos:

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).

Discussion of straightening and unstraightening for (∞,n)-categories:

Last revised on July 17, 2023 at 06:34:31. See the history of this page for a list of all contributions to it.