Pullback-stable model of fibrewise suspension of fibrations (in simplicial sets, or similar setting)

I'm thick as would be notorious, only you're all too polite to mention; is there something difficult about:

The Universal Example is the suspension of the tautological fibration $$ E \to \mathbf{B}(Aut(F))$$ which comes with a map $$\mathbf{B}(Aut(F)) \to \mathbf{B}(Aut(\Sigma F))$$ over which there is again the tautological fibration $$ E' \to \mathbf{B}Aut(\Sigma F).\tag{*}$$ So take pullbacks of $(\mathrm{*})$ along composites $X \to \mathbf{B}(Aut(F)) \to \mathbf{B}(Aut(\Sigma F))$ as the definition of fiberwise suspension.

One idea would be to try to mimic what happens in cubical type theory (CCHM). There fillers are added for "homogeneous" filling problems only. The analogue here of that concept seems to be the following. Consider using the small object argument with filling problems for horns of simplices in the standard way, but use just those horns that omit the i-th face, for some i, and such that the map from the simplex to the base factors through the degeneracy map $s_{i-1}$ or $s_i$. When the pushout is formed from such a filling problem, the two new cells (the i-th face and the whole simplex) map to the same simplex of the base, up to degeneracy. Thus when basechange is performed, both survive or neither survive. If both survive, they are captured by a filling problem of the same form over the new base.

This is a long comment which becomes longer and longer while I answer to the comment’s comments.

Take $U$ to be Voevodsky’s univalent universe classifying Kan fibrations with small fibers. There is the universal Kan fibration $U_\bullet\to U$. I recall that a map from $B$ to $U$ is precisely a Kan fibration $p:X\to B$ together with choices of pull-backs along each map $B'\to B$. This is why having a construction compatible with pull-backs must come from an operator on $U$. The question of functoriality is thus related with the description of maps between fibrations using universes.

Since $U$ is the $\infty$-groupoid of small $\infty$-groupoids (in the setting of $\infty$-categories provided by the Joyal model structure), there is a map $\Sigma:U\to U$ which is the the restriction of the classical suspension functor. Pulling back the universal fibration along $$\Sigma:U\to U$$ defines a new Kan fibration that deserves to be called the universal fiberwise suspension. Whenever a Kan fibration $p:X\to Y$ is classified by a map $f:Y\to U$ then pulling back the universal fiberwise suspension along $f$ defines the fiberwise suspension of $p$. By construction of $U$, this construction is obviously compatible with pull-backs (up to equality), once these have been specified for each fibration $p$.

So far, it is essentially the same answer as the one of Jesse McKeown, except that the universal Kan fibration is not classified by a map to $BAut(F)$ for any $F$ because the universal fibration can have any small Kan complex as fiber (there are Kan fibration with more than one fiber). The description above might give some insights about the obstructions to make this functorial. Indeed, the universe $U$ alone is not sufficient to express functoriality: it encodes only invertible maps between (homotopy) types. But there is a larger universe which classifies $\infty$-categories $S$ and which comes equipped with the universal left fibration $S_\bullet\to S$ of which $U_\bullet\to U$ is the pullback along the inclusion $U\subset S$ (concretely, $S$ is defined as Voevodsky's $U$ except that it classifies left fibrations; it was introduced by Josh Nichols-Barrer in 2007). If we have two Kan fibrations $p_i:X_i\to B$ on the same space which are classified by two maps $f_i:B\to U\subset S$, $i=0,1$, a map from $p_0$ to $p_1$ may be seen as a map from $f_0$ to $f_1$ in the $\infty$-category $Fun(B,S)$, i.e. a morphism of simplicial sets $f:\Delta^1\times B\to S$. The latter classifies a left fibration $q:Y\to \Delta^1\times B$ whose fiber at $i$ is $X_i$. There exists a map $\phi:\Delta^1\times X_0\to Y$ such that $\phi_{|\{0\}\times X_0}$ is the inclusion of $X_0$ into $Y$ and such that $q\phi=1_{\Delta^1}\times p_0$. The fiber of $\phi$ at $1$ gives a map $$X_0\to X_1$$ but the formation of the latter really relies on a contractible space of choices (namely the space of $\phi's$ as above), and there is really no reason to make that more canonical (again, one can do this for the universal map between Kan fibrations, but this does not makes it a bijective correspondence: only an homotopy equivalence between the mapping space of maps from $X_0$ to $X_1$ over $B$ and the space of maps from $f_0$ to $f_1$). The suspension can be defined as a map $$\Sigma : S\to S$$ and this shows how functorial the suspension can be : it is compatible with maps which come from left fibrations to $\Delta^1\times B$ as above. All maps are obtained in this way, but only up to homotopy.

On the other hand, if we had a suspension defined functorially for all Kan fibrations in way which is compatible with pullbacks, that would define an operator $\Sigma:S\to S$ as above : but what I described above is an explicit way to see how the classification of Kan fibrations through maps $B\to U$ is not functorial: the obstruction consists to go from the language of maps $X_0\to X_1$ over $B$ to the language of Kan fibrations $Y\to\Delta^1\times B$, and I don't see why we should even hope that there is 1-to-1 correspondence (as opposed to an homotopy equivalence). In other words, this is where an obstruction should be looked for. I do realize that there is no need to make such 1-to-1 correspondence.

However, I want to emphasize that this question is very related to the problem of turning a « universe-like » functoriality into a « classical » one. More generally, one could ask for a way to take fibrant replacements compatible with pull-backs. This would solve the problem indeed. As Mike Shulman allude below in the comments, such technics are available for some version of the homotopy theory of cubical sets. However, this does not give any evidence that we could succeed for classical simplicial sets. The reason is that the uniform small object argument (which relies on Richard Garner’s generalization of the small object argument) can only be used in the case where the model structure has very peculiar properties, one of them being that there is a representable interval, the Cartesian product with which preserves representable presheaves. This means that we may survive with some versions of symmetric cubical sets as well as with symmetric simplicial sets (this is what is currently developed by Coquand, Sattler, Gambino and others). However, none of these constructively proved model structures are models for classical homotopy types. Furthermore, to my knowledge, all proofs that some models for classical homotopy types define a semantic of homotopy type theory with a univalent universe heavily use the axiom of choice. This means that, in these contexts, the fact that the universe is well behaved strongly relies on the axiom of choice. For me (although I realize this is only a feeling) this is a rather strong evidence that a compatibility between « universe like » functoriality and « classical » functoriality is not something we should expect for classical simplicial sets nor for non-symmetric versions of cubical sets, for instance.