If $C$ is a simplicial model category (I have simplicial commutative rings in mind), then one can simplicially enrich pro-$C$ over sSet by taking $$\lim_j \mathrm{colim}_i \underline{\mathrm{Hom}}_C(A_i,B_j)$$ for any two pro-systems $A_i$ and $B_j$. Note $\underline{\mathrm{Hom}}$ here denotes the enrichment. These are indexed over small cofiltered indexing categories. This is for example done by Isaksen when he defines a model structure on pro-$C$ given that $C$ is proper.
My question is why this isn't $$\mathrm{holim}_j\mathrm{hocolim}_i\underline{\mathrm{Hom}}_C(A_i,B_j) .$$ Homotopy colimits over filtered indexing categories are presented by the strict colimit (maybe you need some condition on $C$ like combinatorial), so this doesn't cause an issue, but what about the homotopy limit?
For example, Galatius and Venkatesh show in their paper "Derived Galois Deformation Rings" that the natural map lim $\to$ holim in the above definition is a weak equivalence (in the Quillen model structure) of simplicial sets if
- $J$ is cofinite (i.e. $\{j : j < j_0\}$ is finite for all $j_0 \in J$),
- each $B_j$ is cofibrant, and
- The maps $B_{j_0} \to \lim_{j<j_0} B_j$ are fibrations for all $j_0$.
In Isaksen's language this means that $B_j$ is strongly fibrant.
But since these conditions on $J$ and $B_j$ are not always satisfied (well, the first one is, without loss of generality), I wouldn't expect holim to give lim all this time. So is there some conceptual explanation of why one would take lim instead of holim in the definition?