nLab
(infinity,1)-Grothendieck construction

Contents

Idea

The (,1)-Grothendieck construction is a generalization of the Grothendieck construction – which establishes an equivalence

Fib(C)2Func(C op,Cat)Fib(C) \simeq 2Func(C^{op}, Cat)

and

Fib Grpd(C)2Func(C op,Grpd)Fib_{Grpd}(C) \simeq 2Func(C^{op}, Grpd)

between fibered categories/categories fibered in groupoids and pseudofunctors to Cat/to Grpd – from category theory to (∞,1)-category-theory.

The Grothendieck construction for ∞-groupoids constitutes an equivalence of (∞,1)-categories

RFib(C)Func(C op,Grpd)RFib(C) \simeq \infty Func(C^{op}, \infty Grpd)

between right fibrations of quasi-categories and (∞,1)-functors to ∞ Grpd, while the full Grothendieck construction for (∞,1)-categories constitutes an equivalence

CartFib(C)Func(C op,(,1)Cat)CartFib(C) \simeq \infty Func(C^{op}, (\infty,1)Cat)

between Cartesian fibrations of quasi-categories and (∞,1)-functors to (∞,1)Cat.

This correspondence may be modeled

For fibrations in -groupoids

The generalization of a category fibered in groupoids to quasi-category theory is a right fibration of quasi-categories.

Theorem

((,0)-Grothendieck construction)

Let C be an (∞,1)-category. There is an equivalence of (∞,1)-categories

RFib(C)Func(C op,Grpd)RFib(C) \simeq Func(C^{op}, \infty Grpd)

where

In the next section we discuss how this statement is presented in terms of model categories.

Model category presentation

We discuss a presentation of the (,0)-Grothendieck construction by a simplicial Quillen adjunction between simplicial model categories. (HTT, section 2.2.1).

Definition

(extracting a simplicial presheaf from a fibration)

Let

In particular we will be interested in the case that ϕ is the identity, or at least an equivalence, identifying C with τ hc(S).

For any object (p:XS) in sSet/S consider the sSet-category K(ϕ,p) obtained as the (ordinary) pushout in SSet Cat

τ hc(X) τ hc(X ) ϕ(p) C K(ϕ,p),\array{ \tau_{hc}(X) &\stackrel{}{\to}& \tau_{hc}(X^{\triangleright}) \\ {}^{\mathllap{\phi(p)}}\downarrow && \downarrow \\ C &\to& K(\phi,p) } \,,

where X =X{v} is the join of simplicial sets of X with a single vertex v.

Using this construction, define a functor, the straightening functor,

St ϕ:sSet/S[C op,sSet]St_\phi : sSet/S \to [C^{op}, sSet]

from the overcategory of sSet over S to the enriched functor category of sSet-enriched functors from C op to sSet by defining it on objects (p:XS) to act as

St ϕ(X):=K(ϕ,p)(,v):C opSSet.St_\phi(X) := K(\phi,p)(-,v) : C^{op} \to SSet \,.
Example

The straightening functor effectively computes the fibers of a Cartesian fibration (p:XC) over every point xC. As an illustration for how this is expressed in terms of morphisms in that pushout, consider the simple situation where

  • C=* only has a single point;

  • X={abc} is a category with three objects, two of them connected by a morphism

  • p:XC is the only possible functor, sending everything to the point.

Then

  • C ={a b c v}

and

  • X XC={ v}

Therefore the category of morphisms in this pushout from * to v is indeed again the category {abc}.

More on this is at Grothendieck construction in the section of adjoints to the Grothendieck construction.

Proposition

With the definitions as above, let π:CC be an sSet-enriched functor between sSet-categories. Write

π !:[C op,sSet][C op,sSet]\pi_! : [C^{op}, sSet] \to [{C'}^{op}, sSet]

for the left sSet-Kan extension along π.

There is a natural isomorphism of the straightening functor for the composite πϕ and the original straightening functor for ϕ followed by left Kan extension along π:

St πϕπ !St ϕ.St_{\pi \circ \phi} \simeq \pi_! \circ St_\phi \,.

This is HTT, prop. 2.2.1.1.. The following proof has kindly been spelled out by Harry Gindi.

Proof

We unwind what the sSet-categories with a single object adjoined to them look like:

let

F:C opsSetF : C^{op} \to sSet

be an sSet-enriched functor. Define from this a new sSet-category C F by setting

  • Obj(C F)=Obj(C){ν}

  • C F(c,d)={C(c,d) forc,dObj(C) F(c) forcObj(c)andd=ν forc=νanddObj(C) * forc=d=ν

The composition operation is that induced from the composition in C and the enriched functoriality of F.

Observe that the sSet-category K(ϕ,p) appearing in the definition of the straightening functor is

K(ϕ,p)C St ϕ(X)K(\phi,p) \simeq C_{St_\phi(X)}

(because K(ϕ,p) is C with a single object ν and some morphisms to ν adjoined, such that there are no non-degenerate morphisms originating at ν, we have that K(ϕ,p) is of form C F for some F; and St ϕ(X) is that F by definition).

To prove the proposition, we need to compute the pushout

τ hc(X) τ hc(X ) C K(ϕ,p)=C St ϕ(X) π C Q\array{ \tau_{hc}(X) &\to& \tau_{hc}(X^{\triangleright}) \\ \downarrow && \downarrow \\ C &\to& K(\phi,p) = C_{St_\phi(X)} \\ {}^{\mathllap{\pi}}\downarrow && \downarrow \\ C' &\to& Q }

and show that indeed QC π !St ϕ(X).

Using the pasting law for pushouts (see pullback) we just have to compute the lower square pushout. Here the statement is a special case of the following statement: for every sSet-category of the form C F, the pushout of the canonical inclusion CC F along any sSet-functor π:CC is C π !F.

This follows by inspection of what a cocone

C ι C F π d C r Q\array{ C &\stackrel{\iota}{\to}& C_F \\ {}^{\mathllap{\pi}}\downarrow && \downarrow^{\mathrlap{d}} \\ C' &\underset{r}{\to}& Q }

is like: by the nature of C F the functor d is characterized by a functor d C:CQ, an object d(ν)Q together with a natural transformation

F(c)Q(d C(c),d(ν))F(c) \to Q(d|_C(c), d(\nu))

being the component F c,ν:C F(c,ν)Q(d(c),d(ν)) of the sSet-functor.

We may write this natural transformation as

F(d C) *Q(,d(ν))=ι *d *νQ(,d(ν)),F \to (d|_C)^* Q(-,d(\nu)) = \iota^* d^* \nu Q(-,d(\nu)) \,,

where d * etc. means precomposition with the functor d.

By commutativity of the diagram this is

π *r *Q(,d(ν)).\cdots \simeq \pi^* r^* Q(-,d(\nu)) \,.

Now by the definition of left Kan extension π ! as the left adjoint to prescomposition with a functor, this is bijectively a transformation

η:π !Fr *Q(,d(ν)).\eta : \pi_! F \to r^* Q(-,d(\nu)) \,.

Using this we see that we may find a universal cocone by setting Q:=C π !F with r:CQ the canonical inclusion and C FC π !F given by π on the restriction to C and by the unit Fπ *π !F on C F(c,ν). For this the adjunct transformation η is the identity, which makes this universal among all cocones.

Proposition

This functor has a right adjoint

Un ϕ:[C op,sSet]sSet/S,Un_\phi : [C^{op}, sSet] \to sSet/S \,,

that takes a simplicial presheaf on C to a simplicial set over S – this is the unstraightening functor.

Proof

One checks that St ϕ preserves colimits. The claim then follows with the adjoint functor theorem.

Theorem

(presentation of the (,0)-Grothendieck construction)

The straightening and the unstraightening functor constitute a Quillen adjunction

(St ϕUn ϕ):sSet/SSt ϕUn ϕ[C op,sSet](St_\phi \dashv Un_\phi) : sSet/S \stackrel{\overset{Un_{\phi}}{\leftarrow}}{\underset{St_\phi}{\to}} [C^{op}, sSet]

between the model structure for right fibrations and the global projective model structure on simplicial presheaves on S.

If ϕ is a weak equivalence in the model structure on simplicial categories then this Quillen adjunction is a Quillen equivalence.

This is HTT, theorem 2.2.1.2.

This models the Grothendieck construction for ∞-groupoids in the following way:

Hence the unstraightening functor is what models the Grothendieck construction proper, in the sense of a construction that generalizes the construction of a fibered category from a pseudofunctor.

Remark: (,0)-fibrations over an -groupoid

Observation

Let C itself be an -groupoid. Then RFib(C)Grpd/C and hence

Grpd/C[C op,Grpd].\infty Grpd/C \simeq [C^{op}, \infty Grpd] \,.
Proof

By the fact that there is the standard model structure on simplicial sets we have that every morphism of -groupoids XC factors as

X X^ fib C,\array{ X &&\stackrel{\simeq}{\to}&& \hat X \\ & \searrow && \swarrow_{\mathrlap{fib}} \\ && C } \,,

where the top morphism is an equivalence and the right morphism a Kan fibration. Moreover, as discussed at right fibration, over an -groupoid the notions of left/right fibrations and Kan fibrations coincide. This shows that the full sub-(∞,1)-category of Grpd/X on the right fibrations is equivalent to all of Grpd/X.

For general fibered (,1)-categories

The generalization of a fibered category to quasi-category theory is a Cartesian fibration of quasi-categories.

Theorem

((,1)-Grothendieck construction)

Let C be an (∞,1)-category. There is an equivalence

Cart(C)Func(C op,(,1)Cat)Cart(C) \simeq Func(C^{op}, (\infty,1) Cat)

where

In the next section we discuss how this statement is presented in terms of model categories.

Model category presentation

Regard the (∞,1)-category C in its incarnation as a simplicially enriched category.

Let S be a simplicial set, τ hc(S) the corresponding simplicially enriched category (where τ hc is the left adjoint of the homotopy coherent nerve) and let ϕ:τ hc(S)C be an sSet-enriched functor.

Definition

(extracting a marked simplicial presheaf from a marked fibration) (HTT, section 3.2.1)

The straightening functor

St ϕ:sSet +/S[C op,sSet +]St_\phi : sSet^+/S \to [C^{op}, sSet^+]

from marked simplicial sets over S to marked simplicial presheaves on C op is on the underlying simplicial sets (forgetting the marking) the same straightening functor as above.

On the markings the functor acts as follows.

Each edge f:de of XsSet/S gives rise to an edge f˜St ϕ(X)(d)=K(ϕ,p)(d,v): the join 2-simplex fv of X

d f e d˜ f˜ e˜ v\array{ d && \stackrel{f}{\to} && e \\ & {}_{\mathllap{\tilde d}}\searrow & \stackrel{\tilde f}{\Rightarrow} & \swarrow_{\mathrlap{\tilde e}} \\ && v }

with image f˜:d˜f *e˜ in the pushout K(ϕ,p)(d,v)=St ϕX(d).

We define the straightening functor to assign that marking of edges which is the minimal one such that all such morphisms f˜ are marked in St ϕX(d), for all marked f:de in X: this means that this marking is being completed under the constraint that St ϕ(X) be sSet-enriched functorial.

For that, recall that the hom simplicial sets of sSet + are the spaces Map (X,Y), which consist of those simplices of the internal hom Map(X,Y):=Y X whose edges are all marked:

Map(X,Y) n=Hom sSet +(X×Δ[n] #,Y).Map(X,Y)_n = Hom_{sSet^+}(X \times \Delta[n]^#, Y) \,.

So we need to find a marking on the St ϕ(X)() such that for all g:Δ[1]C(c,d) the composite

Δ[1]gC(c,d)St ϕ(X)(c,d)Map(St ϕ(X)(d),St ϕ(X)(c))\Delta[1] \stackrel{g}{\to} C(c,d) \stackrel{St_\phi(X)(c,d)}{\to} Map(St_\phi(X)(d), St_\phi(X)(c))

is a marked edge of the mapping complex. By the internal hom-adjunction this edge corresponds to a morphism

St ϕ(X)(g):St ϕ(X)(d)×Δ[1]St ϕ(X)(c)St_\phi(X)(g) : St_\phi(X)(d) \times \Delta[1] \rightarrow St_\phi(X)(c)

and to be marked needs to carry edges of the form f˜×{01} i.e. 1-cells (f˜,Id):Δ[1]St ϕ(X)(d)×Δ[1] to marked edges

g *f˜:Δ[1](f˜,Id)St ϕ(X)(d)×Δ[1]St ϕ(X)(g)St ϕ(X)(c)g^* \tilde f : \Delta[1] \stackrel{(\tilde f,Id)}{\to} St_\phi(X)(d)\times \Delta[1] \stackrel{St_\phi(X)(g)}{\to} St_{\phi}(X)(c)

in St ϕ(X)(c). So we need to ensure that the edges of this form are marked:

we define that the straightening functor marks an edge in St ϕ(X)(c) iff it is of this form g *f˜, for f:de a marked edge of X and gC(c,d) 1.

As in the unmarked cae, the straightening functor has an sSet-right adjoint, the unstraightening functor

n ϕ:[C op,sSet +]sSet +/S.n_\phi : [C^{op}, sSet^+] \to sSet^+/S \,.

This functor Un ϕ exhibits the (,1)-Grothendieck-construction proper, in that it constructs a Cartesian fibration from a given (,1)-functor:

Theorem

(presentation of (,1)-Grothendieck construction)

This induces a Quillen adjunction

(St ϕUn ϕ):SSet +/SSt ϕUn ϕ[C op,SSet +](St_\phi \dashv Un_\phi) : SSet^+/S \stackrel{\overset{Un_{\phi}}{\leftarrow}}{\underset{St_\phi}{\to}} [C^{op}, SSet^+]

between the model structure for Cartesian fibrations and the projective global model structure on functors with values in the model structure on marked simplicial sets.

If ϕ is an equivalence in the model structure on simplicial categories then this Quillen adjunction is a Quillen equivalence.

Proof

This is HTT, theorem 3.2.0.1.

Over an ordinary category

In the case that C happens to be an ordinary category, the (,1)-Grothendieck construction can be simplified and given more explicitly.

This is HTT, section 3.2.5.

Definition

(relative nerve functor)

Let C be a small category and let f:CsSet be a functor. The simplicial set N f(C), the relative nerve of C under f is defined as follows:

an n-cell of N f(C) is

  1. a functor σ:[n]C;

  2. for every [k][n] a morphism τ(k):Δ[k]f(σ(k));

  3. such that for all [j][k][n] the diagram

    Δ[j] τ(j) f(σ(j)) f(σ(jk)) Δ[k] τ(k) f(σ(k))\array{ \Delta[j] &\stackrel{\tau(j)}{\to}& f(\sigma(j)) \\ \downarrow && \downarrow^{\mathrlap{f(\sigma(j\to k))}} \\ \Delta[k] &\stackrel{\tau(k)}{\to}& f(\sigma(k)) }

    commutes.

There is a canonical morphism

N f(C)N(C)N_f(C) \to N(C)

to the ordinary nerve of C, obtained by forgetting the τs.

This is HTT, def. 3.2.5.2.

Remark

When f is constant on the point, then N f(C)N(C) is an isomorphism of simplicial sets, so N f(C) this is the ordinary nerve of C.

The fiber of N f(C)N(C) over an object cC is given by taking σ to be constant on C. Then all the τs are fixed by the maximal τ(n):Δ[n]f(c). So the fiber of N f(C) over c is f(c).

Definition

(marked relative nerve functor)

Let C be a small category. Define a functor

sSet +/N(C)[C,sSet +]:N +sSet^+/N(C) \leftarrow [C, sSet^+] : N^+

by

(CFsSet +)(N f(C),E F),(C \stackrel{F}{\to} sSet^+) \mapsto (N_f(C), E_F) \,,

where f:C opFsSet +sSet is F with the marking forgotten, where N f(C) is the relative nerve of C under f, and where the marking E F is given by …

This is HTT, def. 3.2.5.12.

This functor has a left adjoint +. The value of +(F) on some cC is equivalent to the value of St(F).

This is HTT, Lemma 3.2.5.17.

Proposition

((,1)-Grothendieck construction over a category)

The adjunction

( +N +):sSet /N(C) +N + +[C,sSet +].(\mathcal{F}^+ \dashv N^+) : sSet^+_{/N(C)} \stackrel{\overset{\mathcal{F}^+}{\to}}{\underset{N^+}{\leftarrow}} [C,sSet^+] \,.

is a Quillen equivalence between the model structure for coCartesian fibrations and the projective global model structure on functors.

Proof

This is HTT, prop. 3.2.5.18.

Relation beween the model structures

Theorem (HTT, section 3.1.5)

Let S be a simplicial set.

There is a sequence of Quillen adjunctions

(sSet/S) JoyalsSet +/S(sSet +/S) loc(sSet/S) rfib(sSet/S) Quillen.(sSet/S)_{Joyal} \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}} sSet^+/S \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}} (sSet^+/S)^{loc} \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}} (sSet/S)_{rfib} \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}} (sSet/S)_{Quillen} \,.

Where from left to right we have

  1. the model structure on an overcategory for the Joyal model structure for quasi-categories;

  2. the model structure for Cartesian fibrations;

  3. some localizaton of the model structure for Cartesian fibrations;

  4. the model structure for right fibrations

  5. the model structure on an overcategory for the Quillen model structure on simplicial sets;

The first and third Quillen adjunction here is a Quillen equivalence if S is a Kan complex.

Examples

Cartesian fibrations over the point

For the base category S being the point S=*, the (,1)-Grothendieck construction naturally becomes essentially trivial. However, its model by the Quillen functor

St ϕ:sSet/*sSet[*,sSet]sSetSt_\phi : sSet/* \simeq sSet \to [*,sSet] \simeq sSet

is not entirely trivial and in fact produces a Quillen auto-equivalence of sSet Quillen with itself that plays a central role in the proof of the corresponding Quillen equivalence over general S.

Definition

Let Q:ΔsSet be the cosimplicial simplicial set given by

Q[n]:=J n(x,v),Q[n] := |J^n|(x,v) \,,

where

J n=C (Δ[n]{x}).J^n = C^{\triangleleft}(\Delta[n] \to \{x\}) \,.

Then: nerve and realization associated to Q yield a Quillen equivalence of sSet Quillen with itself.

HTT, section 2.2.2.

Cartesian fibrations over the interval

A Cartesian fibration p:KΔ[1] over the 1-simplex corresponds to a morphism Δ[1] op (∞,1)Cat, hence to an (∞,1)-functor F:DC.

By the above procedure we can express F as the image of p under the straightening functor. However, there is a more immediate way to extract this functor, which we now describe.

First recall the situation for the ordinary Grothendieck construction: given a Grothendieck fibration K{01}, we obtain a functor f:K 1K 0 between the fibers, by choosing for each object dK 1 a Cartesian morphism e dd. Then the universal property of Cartesian morphism yields for every morphism d 1d 2 in K 1 the unique left vertical filler in

e d 1 d 1 e d 2 d 2.\array{ e_{d_1} &\to& d_1 \\ \downarrow && \downarrow \\ e_{d_2} &\to& d_2 } \,.

And again by universality, this assignment is functorial: K 1K 0.

Diagrammatically, the choice of Cartesian morphisms here is a lift e in the diagram

K 1 K e K 1×{01} {01}.\array{ K_1 &\hookrightarrow& K \\ \downarrow &\nearrow_e& \downarrow \\ K_1 \times \{0 \to 1\} &\to& \{0 \to 1\} } \,.

This diagrammatic way of encoding the functor associated to a Grothendieck fibration over the interval generalizes straightforwardly to the quasi-category context.

Definition

Given a Cartesian fibration p:KΔ[1] with fibers the quasi-categories C:=K 0 and D:=K 1, an (,1)-functor associated to the Cartesian fibration p is a functor f:DC such that there exists a commuting diagram in sSet

D×Δ[1] F K p Δ[1]\array{ D \times \Delta[1] &&\stackrel{F}{\to}&& K \\ & \searrow && \swarrow_{\mathrlap{p}} \\ && \Delta[1] }

such that

More generally, if we also specify possibly nontrivial equivalences of quasi-categories h 0:CK 0 and h 1:DK 1, then a functor is associated to K and this choice of equivalences if the first twoo conditions above are generalized to

  • F 1=h 1;

  • F 0=h 0f;

This is HTT, def. 5.2.1.1.

Proposition

For p:KΔ[1] a Cartesian fibration, the associated functor exists and is unique up to equivalence in the (∞,1)-category of (∞,1)-functors Func(K 0,K 1).

Proof

This is HTT, prop 5.2.1.5.

Set C:=K 0 and D:=K 1.

With the notation described at model structure for Cartesian fibrations, consider the commuting diagram

D ×{1} K p D ×Δ[1] # Δ[1] #\array{ D^\flat \times \{1\} &\hookrightarrow& K^{\sharp} \\ \downarrow && \downarrow^{\mathrlap{p}} \\ D^{\flat} \times \Delta[1]^{#} &\to& \Delta[1]^# }

in the category sSet + of marked simplicial sets.

Here the left vertical morphism is marked anodyne: it is the smash product of the marked cofibration (monomorphism) Id:D D with the marked anodyne morphism Δ[1] #Δ[0]. By the stability properties discussed at Marked anodyne morphisms, this implies that the morphism itself is marked anodyne.

As discussed there, this means that a lift d:D ×Δ[1] #K against the Cartesian fibration in

D ×{1} K s p D ×Δ[1] # Δ[1] #\array{ D^\flat \times \{1\} &\hookrightarrow& K^{\sharp} \\ \downarrow &\nearrow_{s}& \downarrow^{\mathrlap{p}} \\ D^{\flat} \times \Delta[1]^{#} &\to& \Delta[1]^# }

exists. This exhibits an associated functor f:=s 0.

Suppose now that another associated functor f is given. It will correspondingly come with its diagram

D ×{1} K s p D ×Δ[1] # Δ[1] #.\array{ D^\flat \times \{1\} &\hookrightarrow& K^{\sharp} \\ \downarrow &\nearrow_{s'}& \downarrow^{\mathrlap{p}} \\ D^{\flat} \times \Delta[1]^{#} &\to& \Delta[1]^# } \,.

Together this may be arranged to a diagram

D ×Λ[2] 2 (s,s) K q p D ×Δ[2] # Δ[1] #,\array{ D^\flat \times \Lambda[2]_2 &\stackrel{(s,s')}{\to}& K^{\sharp} \\ \downarrow &\nearrow_{q}& \downarrow^{\mathrlap{p}} \\ D^{\flat} \times \Delta[2]^{#} &\to& \Delta[1]^# } \,,

where the top horizontal morphism picks the 2-horn in K whose two edges are labeled by s and s, respectively.

Now, the left vertical morphism is still marked anodyne, and hence the lift k exists, as indicated. Being a morphism of marked simplicial sets, it must map for each dD the edge {d}×{01} to a Cartesian morphism in K, and due to the commutativity of the diagram this morphism must be in K 0, sitting over {0}. But as discussed there, a Cartesian morphism over a point is an equivalence. This means that the restriction

k D×{01}K 0k|_{D \times \{0 \to 1\}} \to K_0

is an invertible natural transformation between f and f, hence these are equivalent in the functor category.

Conversely, every functor f:DC gives rise to a Cartesian fibration that it is associated to, in the above sense.

Proposition

Every (,1)-functor f:DC is associated to some Cartesian fibration p:KΔ[1], and this is unique up to equivalence.

Proof

This is HTT, prop 5.2.1.3.

The idea is that we obtain K from first forming the cylinder D×Δ[1] and the identifying the left boundary of that with C, using f.

Formally this means that we form the pushout

N:=(D ×Δ[1] #) D ×{0} #C N := (D^\sharp \times \Delta[1]^#) \coprod_{D^\sharp \times \{0\}^#} C^\sharp

in sSet +, where C and D are C and D with precisely the equivalences marked. This comes canonically with a morphism

NΔ[1]N \to \Delta[1]

and does have the property that N 0=C, N 1=D and that f is associated to it in that the restriction of the canonical morphism D×Δ[1]K to the 0-fiber is f. But it may fail to be a Cartesian fibration.

To fix this, use the small object argument to factor NΔ[1] as

NKΔ[1] #,N \to K \to \Delta[1]^# \,,

where the first morphism is marked anodyne and the second has the right lifting property with respect to all marked anodyne morphisms and is hence (since every morphism in Δ[1] # is marked) a Cartesian fibration.

It then remains to check that f is still associated to this KΔ[1] #. This is done by observing that in the small object argument K is built succesively from pushouts of the form

A N α B N α+1 Δ[1],\array{ A &\to& N_\alpha \\ \downarrow && \downarrow & \searrow \\ B &\to& N_{\alpha+1} &\to& \Delta[1] } \,,

where the morphisms on the left are the generators of marked anodyne morphisms (see here). from this one checks that if the fiber N α× Δ[1]{0} is equivalent to C, then so is N α+1× Δ[1]{0} and similarly for D. By induction, it follows that f is indeed associated to KΔ[1].

To see that the K obtained this way is unique up to equivalence, consider…

Cartesian fibrations over simplices

… for the moment see HTT, section 3.2.2

The universal Cartesian fibration

for the moment see

References

The construction for -groupoid fibrations i.e. left/right fibrations is the content of section 2.2.1, that of quasi-category fibrations i.e. Cartesian fibrations that of section 3.2 in

Revised on June 28, 2012 16:54:36 by Stephan Alexander Spahn (79.227.142.182)