#### [SOLVED] Does the Grothendieck construction satisfy Fubini's thorem

Suppose we are given a functor

$$F:(A\times B)^{\operatorname{op}}\to \operatorname{Set}$$.

It's well-known that the Grothendieck construction in this case evaluates as

$$\int_{A\times B}F = (A\times B)/F$$.

We could also apply this construction pointwise to obtain a functor

$$\int_A F:B^{op}\to \operatorname{Cat}$$

sending $$b\mapsto A/F(b)$$

and similarly

$$\int_B F:A^{op}\to \operatorname{Cat}$$

We can apply the Grothendieck construction again to each of these functors to obtain categories

$$\int_A\int_B F$$

and

$$\int_B\int_A F$$

Is it the case that $$\int_A \int_B F\cong \int_B \int_A F\cong \int_{A\times B} F$$?

#### @David White 2019-02-09 15:19:54

Yes. See section 4.2 of this paper by Harpaz and Prasma, which also extends the result to the setting of model categories.

Another good source on these topics is Emily Riehl's book. The Fubini result is extended to the setting of $$n$$-categories by this thesis.

#### @Harry Gindi 2019-02-09 15:27:51

Great, thanks a bunch!