Proof.Presentability of grants the existence of the values .
Lemma 4.3.2.13 ofΒ [Lu1] states that these expressions define a functor, as indicated.
Proposition 4.3.3.7 ofΒ [Lu1] states that this functor satisfies the universal property of being a left adjoint to the restriction .
We thus have the solid diagram among -categories
in which the downward functors are restriction to underlying -categories, these downward functors are fully faithful.
It remains to explain how the -presentability of grants the existence of the dashed horizontal functor making the diagram commute.
We must show that, for each symmetric monoidal functor , and for each based map among finite sets , the diagram of -categories
commutes.
The map is canonically a composition of a surjective active map followed by an injective active map followed by an inert map , and so it is enough to verify commutativity of the above diagram for each such class of maps.
The case of inert maps is obvious, because then is projection and is defined as the -fold product of functors, for .
The case of injective active maps amounts to verifying that carries each monoidal unit to a monoidal unit. This follows because does so and because the over -categories consist solely of the empty manifold, which is the monoidal unity.
The case of surjective active maps follows from the case that is given by , so that is the -fold tensor product.
Well, because is symmetric monoidal, there is a canonical arrow
between functors that we will argue is an equivalence.
This arrow evaluates on as the horizontal one in the following natural diagram in :
The arrow labeled byΒ () is an equivalence precisely because preserves colimits.
By inspection, the -fold disjoint union functor is an equivalence between -categories, for it is essentially surjective and fully faithful.
It follows that the arrow labeled byΒ () is an equivalence, after observing the following commutative diagram among -categories: