3:25 PM
@Dedalus sorry, in fact i misspoke quite early on: opfibrations are equivalent to pseudofunctors to Cat, not ordinary functors. however, these always admit a canonical strictification, which is a left adjoint PseudoFun(C,Cat) <=> Fun(C,Cat) whose unit is a pseudonatural equivalence.
this means that we can compose $OpFibn(C) \xrightarrow{\sim} PseudoFun(C,Cat) \rightarrow Fun(C,Cat)$. the first is a "strict 2-equivalence", and the second is surely also some sort of "weak 2-equivalence" though this is now definitely out of my wheelhouse...

8 hours later…
11:43 PM
Anyone remember when it's true that $S[X\times_Y Z]\simeq Cobar(S[X],S[Y],S[Z])$ for spaces $X\to Y\leftarrow Z$?
I think that if $Y$ is simply connected I can maybe draw this conclusion from something like the strong convergence of the Eilenberg-Moore spectral sequence for stable homotopy, but I'm not sure if it's true more generally.