For various reasons (one of which was adumbrated in my previous post), I have been thinking about generalising the classical notion of ‘weak factorisation system’ to work better in the intuitionistic context.

The difficulty, really, is in how we understand existence. Let us consider a pair of morphisms, say *f* : *A* → *B* and *g* : *C* → *D*, in an elementary topos 𝒮. What does it mean to say that *f* has the left lifting property with respect to *g* in the internal logic of 𝒮? That is, suppose when given morphisms *h* : *A* → *C*, *k* : *B* → *D*, if

- for all
*a*in*A*,*k*(*f*(*a*)) =*g*(*h*(*a*)),

then there exists a morphism *ℓ* : *B* → *C* such that

- for all
*a*in*A*,*ℓ*(*f*(*a*)) =*h*(*a*); and - for all
*b*in*B*,*g*(*ℓ*(*b*)) =*k*(*b*).

Interpreted naïvely, this says that *f* has the left lifting property with respect to *g* in the ordinary sense. Nonetheless, in the internal logic of 𝒮, the above is true when *f* is the unique morphism 0 → 1 and *g* is any epimorphism *C* → *D* – exactly as in the archetypical topos **Set**. On the other hand, it is simply not true that epimorphisms induce surjections of global sections! What the above really says is the following: a lifting exists – *after* base change along an epimorphism!

In light of the preceding discussion, and also bearing in mind the work of Brown, Jardine, Joyal et al. on the homotopy theory of sheaves of simplicial sets, it would appear that the right definition of left/right lifting property in the relative context must be *local*, in the sense of the following definition.

**Definition.** Let 𝒮 be a regular category, let ℂ be an 𝒮-indexed category, let *J* be an object in 𝒮, and let 𝒞^{J} be the fibre of ℂ over *J*. Given morphisms *f* and *g* in 𝒞^{J}, we say *f* has the **local left lifting property** with respect to *g* if, for all morphisms *x* : *I* → *J* in 𝒮 and all morphisms *h* and *k* in 𝒞^{I} such that *k* ∘ *x***f* = *x***g* ∘ *h*, there exist a regular epimorphism *e* : *E* → *I* and a morphism *ℓ* in 𝒞^{E} such that *ℓ* ∘ *e***x***f* = *e***h* and *e***x***g* ∘ *ℓ* = *e***k*.

It is easy to verify that the class of morphisms in 𝒞^{J} that have the local left lifting property with respect to *g* is closed under composition and retracts. It is also closed under finite coproducts and pushouts, provided we restrict attention to those colimits that are stable under reindexing. The distinguishing feature is the descent property: if *x* : *I* → *J* is any regular epimorphism in 𝒮 and *f* is a morphism in 𝒞^{J}, then *f* has the local left lifting property with respect to *g* if and only if *x***f* has the local left lifting property with respect to *x***g*.

Whether or not the class is closed under transfinite composition and 𝒮-indexed coproducts seems rather more tricky. If our metatheory has the axiom of choice, then the class is indeed closed under reindexing-stable transfinite composition; the same can be said for reindexing-stable infinite coproducts. It should therefore be unsurprising that there is a connection between the internal axiom of choice in 𝒮 and the question of whether or not the class is closed under 𝒮-indexed coproducts.

Indeed, suppose 𝒮 is an elementary topos, and consider the self-indexing of 𝒮. We earlier observed that 0 → 1 has the local left lifting property with respect to epimorphisms. Thus, if the class of morphisms with the local left lifting property with respect to epimorphisms is closed under 𝒮-indexed coproducts, then an epimorphism *g* : *C* → *D* must have the local right lifting property with respect to the unique morphism 0 → *D*; but this happens if and only if the morphism [*D*, *g*] : [*D*, *C*] → [*D*, *D*] is an epimorphism, i.e. if and only if *g* : *C* → *D* has a section in the internal logic of 𝒮.

So, should we accept the definition of ‘local lifting property’ proposed above, and with it, the failure of the basic saturation properties of classes of morphisms with a left/right lifting property? Or should we continue searching for a definition that allows us to carry over more of the classical theory?