I went back to the filtered colimit question and worked out the case of pullback preservation. It is mostly a combination of previously discussed techniques. The following presentation is organized linearly. I use left fibration, Kan fibration, etc. in the homotopical sense, i.e. as concepts invariant under equivalence. By a category, I mean a higher category as implemented as complete Segal spaces. Recall the following statement, proved earlier. Lemma 1. Let X be a category. Then the free replacement functor CartFib(X) → RightFib(X) is compatible with base change in X. □ We have the following standard facts. We have a reflective embedding const : Space → sSpace, with reflection given by taking the colimit, i.e. realization. Lemma 2. For a simplicial space X, the right adjoint Space/|X| --[const]-> sSpace/(const |X|) --[pullback]-> sSpace/X to realization is fully faithful. Its image is the Kan fibrations. Proof. Recall that a map Y → X is a Kan fibration exactly if it is a cartesian natural transformation. With this, the statement becomes descend (i.e. the van Kampen condition) for colimits over Δ in Space. In detail, we have the following standard argument. Note that const : Space → sSpace sends arbitrary maps to Kan fibrations. In particular, the right adjoint of the statement is valued in Kan fibrations. Restricting sSpace(X) to KanFib(X), we will show that the unit and counit of the adjunction are invertible. Let A → |X| be a map in Space. Let Y → X be the pullback of its image under const along X → const |X|. Since colimits in Space are stable under pullback, the map Y → const A is a colimiting cocone. That is, its transpose |Y| → A is invertible. This shows that the counit at A → |X| is invertible. Let Y → X be a map in sSpace. To check that the unit at Y → X is invertible, we have to show that the induced square from Y → X to const |Y| → const |X| is a pullback. This is descend. □ Corollary 3. Let Y → X be a map of simplicial spaces. Then |Y| → |X| is invertible exactly if the free replacement of Y → X by a Kan fibration is terminal. Proof. An immediate consequence of Lemma 2 (or Lemma 4 below). □ sSpace carries the *Kan factorization system* whose right class are the Kan fibrations. The maps in the left class we call *Kan left maps*; they are those maps that become invertible under realization (this follows from Lemma 2). It is cofibrantly generated by the maps Δ[a] → Δ[b]. A map X → 1 is in the right class exactly if X is a constant simplicial space. That is, we may identify spaces with Kan fibrant simplicial spaces. Then Lemma 2 may be stated as follows. Lemma 4. Let A → B be a Kan left map with B Kan fibrant. Then the pullback functor KanFib(B) → KanFib(A) is an equivalence. □ Note that the left adjoint to pullback KanFib(B) → KanFib(A) sends Y → A to the right map of the Kan factorization of the composite Y → A → B. The unit is the induced pullback corner map. The counit is given by orthogonality. Corollary 5. Consider a square of Kan fibrations from Y' → X' to Y → X. Assume that Y → X is a Kan left map and that X is Kan fibrant. Then the square is a pullback exactly if Y' → Y is a Kan left map. Proof. This is a direct consequence of Lemma 4. The forward direction follows from invertibility of the counit of the right adjoint KanFib(X') → KanFib(X). The reverse direction follows from invertibility of the unit. □ Remark. One may show that the Kan factorization system is stable, i.e. that Kan left maps are stable under pullback along Kan fibrations. This shows that the assumption of Corollary 5 that X is Kan fibrant can be removed in the forward direction. We will not need this here. One may also observe that Kan fibrations admit a classifier (if we restrict to κ-small maps), the universal map V_Kan → U_Kan of (κ-small) Kan fibrations, and use this to prove descend. Furthermore, U_Kan is itself Kan fibrant. Lemma 6. Realization preserves pullback squares whose vertical maps are Kan fibrations. Proof. This is a consequence of Corollary 5. Consider a pullback square between Kan fibrations Y' → X' and Y → X. We have to show that the square obtained by functorially applying Kan fibrant replacement R is a pullback. By the backward direction of Corollary 5, the square from Y → X to RY → RX is a pullback. By pullback pasting, we may thus reduce to the case where X is Kan fibrant. The map X' → X factors as X' → RX' → X. This pulls back along Y → X to a factorization Y' → Z → Y of Y' → Y. In the pullback square between the Kan fibrations Y' → X' and Z → RX', we have RX' Kan fibrant and a Kan left map X' → RX'. By the forward direction of Corollary 5, the map Y' → Z is a left map. Since Z is Kan fibrant, Y' → Z implements the Kan fibrant replacement Y' → RY'. The pullback square from Z → RX' to Y → X then is the action of applying Kan fibrant replacement to the original square. □ Lemma 7. Let Y → X be a cartesian fibration between categories. Assume that |Y(x)| is terminal for all x ∈ X₀. Then |Y| → |X| is invertible. Proof. Using Corollary 3, it suffices to show that the free Kan fibration on Y → X is terminal. Taking the free Kan fbration factors via taking the free right fibration Y' → X. It will thus suffice to show that Y' → X is the terminal over X, i.e. invertible. By Lemma 1, the fibers of Y' → X are realizations of fibers of Y → X. By assumption, they are terminal, so Y'₀ → X₀ is an equivalence. Since Y' → X is a right fibration, the maps Y'_n → X_n are pullbacks of Y'₀ → X₀, hence equivalences. Hence, Y' → X is an equivalence. □ Remark. The reverse implication does not hold. To see this, consider the cartesian fibration over Λ₀[2] → Δ[2] → Δ[1] where the last map identifies 1 and 2. Remark. Lemma 7 is a higher version of Quillen's Theorem A. Given a functor f : A → B, the free replacement of f by a cartesian fibration is B ↓ f → B. The functor A → B ↓ f is a reflective embedding, hence becomes invertible under realization. So the realization of f is the same as of B ↓ f → B. And the fiber of B ↓ f → B over b ∈ B₀ is given by b ↓ f. So for f to be invertible under realization, it suffices for b ↓ f to be invertible under realization for all b ∈ B₀. Lemma 8. Let Y → X be a cartesian fibration. Assume that its free replacement Y' → X by a right fibration is a Kan fibration. Then pullbacks along Y → X are preserved by realization. Proof. Consider a map M → X. Let N → N' → M be the pullback of Y → Y' → X along M → X. By Lemma 1, this is again the free replacement of a cartesian fibration by a right fibration. Also, N' → M is again a Kan fibration. Note that taking the free Kan fibration factors via taking the free right fibration. Thus, the two factorizations are also free replacements by Kan fibrations. We have to show that the square from |N| → |M| to |Y| → |X| is a pullback. By pullback pasting, this separates into two parts. - The square from |N| → |N'| to |Y| → |Y'| is a pullback. Both maps are invertible since N → N' and Y → Y' are Kan left maps. - The square from |N'| → |M| to |Y'| → |X| is a pullback. This is Lemma 6. □ Let S = {0 → 01 ← 1} denote the walking cospan. By definition, a category C is weakly filtered exactly if the cartesian fibration [S^op ⋆ 1, C] → [S^op, C] has fibers that are terminal under realization. Lemma 9. Let C be a weakly filtered category. Let D → C × C be the free replacement of [S, C] → C × C by a right fibration. Then D → C × C is a Kan fibration. Proof. This is similar to an earlier argument. First, note that [S, C] → C × C is a cartesian fibration. By Lemma 1, the free replacement of a cartesian fibrations by a right fibrations is computed fiberwise. For a map (f₀, f₁) : (x₀, x₁) → (y₀, y₁) in C × C, we have to show that the induced base change map D(y₀, y₁) → D(x₀, x₁) is invertible. By the above, this is the map |[S, C](y₀, y₁)| → |[S, C](x₀, x₁)| induced by (f₀, f₁). We split this as |[S, C](y₀, y₁)| → |[S, C](x₀, y₁)| → |[S, C](x₀, x₁)|. By symmetry, it will suffice to show that the first map is invertible. This is now precisely the statement of an earlier lemma. Let us do the proof in more detail here. Consider the category E whose objects consist of the following data: - an object u under x₀ and y₁, - an object v under the diagram y₀ ← x₀ → u ← y₁. We have forgetful functors from E to [S, C](y₀, y₁) and [S, C](x₀, y₁). By 2-out-of-3, it suffices to show that these become invertible under realization. We can regard E as the category of: - an object v under y₀ and y₁, - a factorization y₁ → u → v of the map y₁ → v, - a lift of the composite x₀ → y₀ → v through u → v. The functor E → [S, C](y₀, y₁) corresponds to the projection to the first component. We have a fully faithful functor [S, C](y₀, y₁) → E sending y₀ → v ← y₀ to the factorization y₁ → u → v where u → v is the identity. The functor E → [S, C](y₀, y₁) is the reflection of this embedding. Since these two functors form an adjunction, they become invertible under realization. Let us look at the functor E → [S, C](x₀, y₁). This is a pullback of the cartesian fibration [S^op ⋆ 1, C] → [S^op, C] along the map [S, C](x₀, y₁) → [S^op, C] sending x₀ → u ← y₁ to y₀ ← x₀ → u. Since C is weakly filtered, its fibers are terminal under realization. By Lemma 7, it becomes invertible under realization. □ Lemma 10. Let A → C ← B be a cospan of simplicial spaces. Let L be its oplax limit. Assume that C is a weakly filtered category. Then the canonical map from |L| to the pullback of |A| → |C| ← |B| is invertible. Proof. The oplax limit L is formally given as the dependent product of the induced cocartesian fibration over S. We may describe it as the pullback of A × B → C × C ← [S, C] where the second map is induced by 0 and 1. The pullback of |A| → |C| ← |B| is the same as the pullback |A × B| → |C × C| ← |[S, C]|. For this, use that realization commutes with products and that the canonical map |C| → |[S, C]| is invertible. It thus suffices to show that the pullback of A × B → C × C ← [S, C] is preserved by realization. Lemma 9 states that the free replacement of the cartesian fibration [S, C] → C × C by a right fibration is a Kan fibration. Thus, the claim follows from Lemma 8. □ Following the previous discussion, the above statement gives the dependent version of Paolo's I-J-formula for I = S and J a cocartesian fibration over S with weakly filtered fibers (actually, it suffices that the fiber over 01 is weakly filtered). We fix the following notation. For a map q : Y → X of simplicial spaces, we have a pullback functor q^* : LeftFib(X) → LeftFib(Y); we denote its left adjoint by q_! and its right adjoint by q_*. We also have q^* : CocartFib(X) → CocartFib(Y); we denote its right adjoint by q_*^cart and its counit eval : q^* q_*^cart → Id. Lemma 11. Let p : C → S be a cocartesian fibration such that C(01) is weakly filtered. Abbreviate P = S_*^cart C. Then for any left fibration X → C, the canonical comparison map P_! (S × P → P)_* eval_C^* X → S_* p_! X is invertible. Proof. For a map q : Y → X of simplicial spaces, write Σ_q and Π_q for the left and right adjoints for pullback. Then q_! = Free_leftfib Σ_q and q_* = Cofree_leftfib Π_q. If q is a cartesian fibration, then Π_q preserves left fibrations, hence q_* = Π_q. With this, the goal map rewrites as Free_leftfib Σ_P Π_(S × P → P) eval_C^* X → Π_S Free_leftfib Σ_p X. Rewriting this using Σ_P Π_(S × P → P) eval_C^* ≃ Π_S Σ_p, the goal map becomes Free_leftfib Π_S Σ_p X → Π_S Free_leftfib Σ_p X. At this point, we generalize and show that Free_leftfib Π_S Y → Π_S Free_leftfib Y is invertible for any cocartesian fibration Y with base S such that Y(01) is weakly filtered. To instantiate, we set Y = Σ_p X. We have Y(01) ≃ Σ_{C(01)} X|_{C(01)}. As the category of elements of a space-valued diagram over a weakly filtered category, it is itself weakly filtered (this was proved earlier). On the left side, the dependent product Π_S Y is given by the oplax limit L of the diagram Y(0) → Y(01) ← Y(1). The free replacement over the point by a left fibration is given by the realization |L|. On the right side, by Lemma 1, Free_leftfib Y is computed fiberwise. Taking the dependent product Π_S, we get the pullback Q of |Y(0)| → |Y(01)| ← |Y(1)|. With this, the goal becomes an instance of Lemma 10. □ Corollary 12. Let J be a weakly filtered category. For any diagram F : S × J → Space, the canonical comparison map colim_{j : [S, J]} lim_{s:S} F(s, j(s)) → lim_{s:S} colim_{j:J} F(s, j) is invertible. Proof. Instantiate Lemma 11 to the cocartesian fibration π₁ : S × J → S. Space-valued diagrams are modelled by left fibrations. Left and right Kan extension along q is modelled by q_! and q_*, respectively. These are computed pointwise by colimits and limits, respectively, since all such appearing q are bicartesian fibrations. □ Corollary 13. Weakly filtered colimits of spaces commute with pullbacks. Proof. In the situation of Corollary 12, the constant map J → [S, J] is a reflective embedding, hence final. So the colimit over [S, J] does not change if we restrict it to J, and we get that the comparison map colim_{j : J} lim_{s:S} F(s, j) → lim_{s:S} colim_{j:J} F(s, j) is invertible. □ Note that we do not need filteredness of J for finality of J → [S, J] in the above argument. In particular, this gives that filtered colimits commute with pullbacks. Products (of arbitrary <κ, if κ-filteredness is assumed) are easy, so this gives at least one possible proof of commutation of κ-filtered colimits and κ-small limits. I wonder if there is a more abstract proof that does not separate κ-small limits into pullbacks and products.