Proof.For there is nothing to prove and so we assume that .
By 4.4.5, it is enough to show that
is -connected where
is the forgetful functor. By 4.3.5, it is
enough to show that has a section and is -connected.
Since , we have and, therefore,
by 5.1.1, has
a section. Thus, we are reduced to showing that the image of
under the functor
is an equivalence. First, we show that
preserves binary products. For , this follows from T.6.5.1.2.
The general case reduces to as by T.6.4.1.5 we can embed
as a full subcategory of an -topos spanned
by the -truncated objects. It follows that we get
a symmetric monoidal functor .
By 5.1.2, the functor
induced by is a left adjoint. Consider the
following (solid) commutative diagram in the homotopy category of
:
where the vertical maps are the forgetful functors and is induced
by restriction along the essentially unique map . Since
is an essentially -category, it follows from 3.1.8
that is an equivalence. Taking to be an inverse of
up to homotopy, the outer rectangle is a commutative square in the
homotopy category of . Therefore, to show that
is an equivalence, it is enough to show that
is an equivalence. In fact, we shall show that
is an equivalence. Note that the composition of the left and then
bottom functors preserves binary products and since the right vertical
functor preserves products and is conservative, it follows that the
top functor also preserves binary products. On the other
hand, also preserves coproducts, since is left adjoint
(by the above discussion) and is an equivalence. Finally, in
, the
canonical map from the coproduct to the product is an equivalence
by A.3.2.4.7.
∎