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

Given a fibration $p : Y \to X$ in simplicial sets (or any other model category), there are various ways to construct its fibrewise suspension, i.e. its suspension as an object of the slice $\newcommand{\SSet}{\mathbf{SSet}}\SSet/X$. Most obviously, one can take a homotopy pushout of $X \leftarrow Y \rightarrow X$, to obtain a non-fibrant model $\newcommand{\pre}{\mathrm{nf}} \Sigma^\pre_X Y \to X$, and then factorise this map as a trivial cofibration followed by a fibration to obtain a fibrant model $\Sigma_X Y \to X$.

However, in general, this construction will not be stable up to isomorphism under pullback in the base, only stable up to weak equivalence. That is, given $p : Y \to X$ as before, and a map $f : X' \to X$, then $f^*(\Sigma_X Y)$ and $\Sigma_{X'} f^*Y$ will be weakly equivalent over $X'$, but not isomorphic. The non-fibrant part $\Sigma^\pre$ can easily be constructed so that it is stable up to iso. But the factorisation step isn’t so stable, at least using off-the-shelf constructions (a general choice of (TC,F) factorisations on the category can’t be pullback-stable in the codomain, for fairly obvious reasons).

Is there an alternative construction of the fibrant fibrewise suspension of a fibration, that is stable up to iso under pullback in the base? Or is there some known obstacle to this?

I’d be most interested in answers for simplicial sets, or some class of model categories including it, or at least of a similar flavour. My motivation is in modelling suspensions and related constructions in type theory (precisely, suspensions axiomatised as a higher inductive type).

• Pardon me; in what category+ do you want the suspension to be fibrant? totalspace fibrant in SSet? fibration fibrant in SSet/X ? ... – Jesse C. McKeown Oct 1 '15 at 22:44
• Could you elaborate on the "fairly obvious reasons" why factorizations cannot be stable? I think I have an idea for a carefully hand-crafted factorization, but the details would be messy... so before I try to check them I want to make sure that I'm not overlooking any obstacles. – Karol Szumiło Oct 2 '15 at 9:35
• I'd suggest using the standard non-fibrant construction of the fiberwise suspension, whose geometric realization is the standard fiberwise suspension in spaces (which preserves fibrations); then pull back the resulting map $Sing |\Sigma_X Y| \to Sing |X|$ along the map $X \to Sing |X|$, since applying the singular complex preserves fibrations. However, this doesn't really work in general model categories. – Tyler Lawson Oct 2 '15 at 15:04
• Actually, I was not careful enough. A fibration $Y \to X$ of simplicial sets only realizes to a quasifibration, and $Sing$ applied to a quasifibration isn't necessarily a fibration -- so this won't fly. Sorry. – Tyler Lawson Oct 2 '15 at 18:15
• Realizations of Kan fibrations are in fact (non-obviously) Serre fibrations. See e.g. 3.6.2 in Hovey's Model Categories. – Karol Szumiło Oct 2 '15 at 18:24

There is an answer to this question in the comments that works for simplicial sets, and more generally for projective model structures on simplicial presheaves. Since 3 years later it hasn't been recorded as an "answer", I thought I would do the service, and provide the references.

For simplicial sets, it suffices to show that given Kan fibrations $$A,B,C$$ over a base $$X$$, and maps $$f:A\to B$$ and $$g:A\to C$$ one of which is a cofibration (a monomorphism), there is a pullback-stable fibrant replacement of the pushout $$B+_A C$$. The fiberwise suspension $$\Sigma_X Y$$ can then be constructed as a pushout of $$X+X \leftarrow Y+Y \to Y\times \Delta^1$$, the latter map being a cofibration. One can similarly construct general homotopy pushouts as double mapping cylinders.

To prove this, apply geometric realization to the whole diagram, landing in some convenient category of topological spaces (e.g. compactly generated). As noted in the comments, Quillen proved that the geometric realization of a Kan fibration is a Serre fibration. Moreover, since a Serre fibration between CW complexes is a Hurewicz fibration (h/t Peter May), in fact the geometric realization of a Kan fibration is a Hurewicz fibration. However, Monica Clapp proved that Hurewicz fibrations are closed under pushouts of cofibrations. Thus, $$|B| +_{|A|} |C| \cong |B+_A C|$$ is again a Hurewicz fibration over $$|X|$$. Now apply the total singular complex, obtaining a Kan fibration $$S|B+_A C| \to S|X|$$, and pull back along the acyclic cofibration $$X \to S|X|$$ to obtain a fibrant model of $$B+_A C$$ over $$X$$. Since geometric realization and total singular complex both preserve finite limits, the whole construction is stable under pullback (up to isomorphism).

Moreover, since all the functors involved are simplicially enriched, the construction can be applied pointwise in a category $$[{\scr C}^{op},\mathrm{sSet}]$$ of simplicial presheaves on any simplicially enriched small category $$\scr C$$ to yield a pointwise-fibrant, i.e. projectively fibrant, model for homotopy pushouts and suspensions that is stable under pullback. Note that the cofibration also only needs to be pointwise, i.e. an injective cofibration rather than a projective one.

I believe this also solves the related problem of size preservation of fibers, since geometric realization and total singular complex both preserve the property of having small fibers. Hence it implies that the universe of Kan fibrations in simplicial sets is closed under HIT pushouts. (Unfortunately, the projective version doesn't help directly for modeling type theory, since projective model structures don't seem to have dependent products or univalent universes.)

• Fantastic — thankyou for sitting down and putting this together and filling in the references! I’d kept on meaning to do that and then not making the time to :-) – Peter LeFanu Lumsdaine Jan 9 at 18:33

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.

• This gives a pullback-stable way of suspending “fibrations specified via a map into $\mathbf{B}(Aut(F))$”, or, more generally, into the base of any pre-specified fibration. But for an abstract fibration $Y \to X$, its expression as a pullback of $E \to \mathbf{B}(Aut(F))$ (or any other fibration) is not unique, and (as far as I can see) this makes it hard to transfer this “universal case” to a stable-up-to-iso suspension for general fibrations. – Peter LeFanu Lumsdaine Oct 2 '15 at 14:05
• Well, that's fair... I don't suppose a univalent universe helps you much? – Jesse C. McKeown Oct 2 '15 at 15:52
• Not that I can see… with a univalent universe, the expression of any other fibration as a pullback becomes unique up to homotopy in an appropriate sense (there’s a precise statment of this in The Simplicial Model of Univalent Foundations), but not unique enough to give stability up to iso. – Peter LeFanu Lumsdaine Oct 2 '15 at 16:00

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.

• Yes, I’d wondered about a construction along these lines — the hard part is proving that the result is a fibration, which I hadn’t managed to do. However, if I understood right, the preprint that Andrew Swan advertised a few weeks ago is doing something like this — I haven’t read it yet, but if it does, I’ll report back here! – Peter LeFanu Lumsdaine Mar 15 '18 at 15:51
• It seems to me that the construction I introduce above (which is compatible with base change) preserves the homotopy type of the fibers of the geometric realization of the map, so a natural conjecture is that a quasifibration of simplicial sets with solutions for all homogeneous filling problems is a fibration. It should be possible to show that the naive (non-fibration) versions of the various higher inductive types all are quasifibrations (when the inputs to them are fibrations), making them suitable inputs for this construction. – Dan Grayson May 1 '18 at 18:00
• Peter, what "preprint that Andrew Swan advertised a few weeks ago" did you mean? – Dan Grayson Jun 6 '18 at 11:56

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.

• Is this functionally different from Jesse's answer? Or put differently, if this works, doesn't Jesse's answer also work? – Mike Shulman Mar 16 '18 at 2:45
• To further amplify on Peter's comment, I think the point is that one can't distinguish between "functoriality" and "pullback-stability". It doesn't make sense to say that we have a "pullback-stable" construction of the suspension of one fibration in isolation; what it means to talk about pullback-stability is that we have an operation assigning to each fibration a suspension of it, such that any pullback of the specified suspension of a fibration is the specified suspension of its pullback. – Mike Shulman Mar 16 '18 at 11:02
• With the universe approach, to define such a suspension operation we have to choose a classifying map for each fibration, and there seems no way to guarantee that these choices will be pullback-stable up to isomorphism (though they certainly will be up to homotopy equivalence). – Mike Shulman Mar 16 '18 at 11:03
• What I meant by "universe approach" is what you and Jesse are suggesting, namely to choose a suspension on the universe and then define a suspension operation by composing with it. It's true that if we had a pullback-stable suspension operation we would get a suspension operation on the universe, but that doesn't imply that we can go the other way. – Mike Shulman Mar 16 '18 at 13:08
• Well, I agree that there certainly isn't a 1-1 correspondence. But I don't think that means there couldn't be some way to choose suspensions in a strictly stable way. For instance, it's basically known now that such a choice is possible for cubical sets, even though I believe the "universe approach" in cubical sets would have the same issue as in simplicial sets. – Mike Shulman Mar 18 '18 at 9:42