Recall that a trivial Kan fibration is a morphism in **sSet** that has the right lifting property with respect to the boundary inclusions ∂Δ^{n} ↪ Δ^{n} for all *n* ≥ 0. The following is well-known:

**Proposition.** A morphism in **sSet** has the left lifting property with respect to all trivial Kan fibrations if and only if it is a monomorphism.

The standard proof uses the fact that monomorphisms in sSet admit a cellular decomposition, and the fact that the class of morphisms that have the left lifting property with respect to another class is closed under transfinite composition, pushouts, and retracts.

Yet, the proposition is equivalent to the axiom of choice! Indeed, let ∇ : **Set** → **sSet** be the right adjoint of the functor *X* ↦ *X*_{0}. (∇ is also known as cosk_{0}.) It is clear that, if *f* : *X* → *Y* is a surjection, then ∇*f* : ∇*X* → ∇*Y* is a trivial Kan fibration: indeed, *f* : *X* → *Y* is a surjection if and only if ∇*f* : ∇*X* → ∇*Y* has the right lifting property with respect to ∂Δ^{0} ↪ Δ^{0}, and for *any* map *f* : *X* → *Y*, ∇*f* : ∇*X* → ∇*Y* has the *unique* right lifting property with respect to ∂Δ^{n} ↪ Δ^{n} for all *n* ≥ 1. But 0 → ∇*Y* is a monomorphism, so if the proposition holds, then ∇*f* : ∇*X* → ∇*Y* must have a section; and ∇ : **Set** → **sSet** is fully faithful, so *f* : *X* → *Y* has a section if and only if ∇*f* : ∇*X* → ∇*Y* has a section.

A few minutes thinking should reveal where we use the axiom of choice in the proof of the proposition. While it is true that every monomorphism in **sSet** is a relative cell complex (provided you allow arbitrarily many cells to be attached at each stage), it would appear that we need the axiom of choice to deduce that every relative cell complex is in the class of morphisms generated by the boundary inclusions under transfinite compositions and pushouts: after all, we have to choose the order in which we attach the cells!

But that is not the end of the story: if that were the only problem, then we could deduce that trivial Kan fibrations have the right lifting property with respect to monomorphisms in **sSet** whose codomain is well-orderable. This is not obviously true either – in fact, it seems that we need the axiom of choice to show that the class of morphisms with the left lifting property with respect to another class is closed under coproducts and transfinite composition!

So perhaps the moral of the story is that the theory of cofibrantly-generated model categories is non-constructive in subtle, easily missed ways.

“whose codomain is well-orderable”

shouldn’t that be “well-ordered”? Or perhaps I am thinking of the stronger step of trying to get a Kan fibration analogue of one of Nikolaus’ algebraic Kan complexes.

How about the small object argument of Richard Garner? I can’t remember if this applies in the case of simplicial sets (I guess not, but I can hope)

A well-orderable simplicial set is one for which a well-ordering of all its simplices exists.

Garner’s small object argument seems to work without AC: as far as I can tell, it doesn’t use the fact that the left class of a weak factorisation system is closed under coproducts and transfinite composition. (The trade-off being that the proof that the left factor has the left lifting property is immensely hard to follow!) I am inclined to believe that the theory of locally finitely presentable categories still makes sense in the absence of AC, and that

sSetis still locally finitely presentable. So I suppose the conclusion one has to draw in that case is that we still have a weak factorisation system, but the class of morphisms with the left lifting property with respect to trivial Kan fibrations is smaller than one expects.