Proof. First, we show that for each there is an equivalence of
-categories
|
|
|
Since is defined simply as the mapping simplicial
set [52, 1.2.7.2], we have the equivalence
|
|
|
Since colimits in functor -categories are computed
pointwise [52, §5.1.2.3] and the -category
is the full subcategory of
spanned by the exact functors, we have a map
|
|
|
and lemma 7.3 implies that it is an equivalence. It
is now straightforward to check that these comparison maps assemble
into the desired simplicial equivalence.
∎