**Edit:** The claim below is wrong, as explained in the comments,
because infinite homotopy products of simplicial sets require their components to be fibrantly replaced first, unlike finite homotopy products.

Simplicial homotopy colimits (i.e., homotopy colimits indexed by the opposite category of simplices) commute with (small) homotopy products in spaces.

This can be easily seen by presenting spaces as simplicial sets, simplicial homotopy colimits as the diagonals of the corresponding bisimplicial sets, homotopy products as products, and observing that the diagonal functor, being induced by a restriction along an inclusion of categories, preserves all (co)limits because (co)limits are computed componentwise in any category of functors. In particular, the diagonal functor commutes with small products, which establishes the desired property.

The same argument extends to all Grothendieck ∞-toposes (e.g., quasicategorical toposes or model toposes), because they can be presented as left Bousfield localizations of the categories of simplicial presheaves on small sites, and homotopy (co)limits are computed componentwise in any category of simplicial presheaves, or a left Bousfield localization thereof.

Of course, the opposite category of simplices is homotopy sifted and homotopy sifted colimits commute with finite homotopy products, so the interesting part is commutation of simplicial homotopy colimits with infinite (but small) homotopy products.

I would like to obtain a model-independent proof of this property. Recall that Grothendieck ∞-toposes can be characterized by the appropriate version of Giraud's axioms, as proposed by Rezk, namely, they are precisely those locally presentable ∞-categories in which homotopy colimits are universal, homotopy coproducts are disjoint, and every groupoid object is effective.

Is it possible to prove that small homotopy products commute with simplicial homotopy colimits directly from Giraud's axioms without resorting to a particular model of spaces?

| is contractible. But the geometric realization of a product of infinitely many copies of X_is not connected: for example, there's no path joining the identity map Z -> Z with the constant map joining Z -> {0} -> Z. (Contradicting your "elementary computation".) $\endgroup$3more comments