A Functorial Weak Factorisation System from Path Types

We show that the path types structure proposed by Awodey and Hua [2] gives rise to a functorial weak factorisation system (WFS). Our work draws on path object factorisations as in [7, 3, 1] and from Gambino and Garner’s identity type weak factorisation system on the syntactic category of dependent type theory [4]. In analogy to the latter, we define our left maps as the maps that left-lift against a single map $𝗍$, representing a universe. Our right maps are then the saturation of $𝗍$ (i.e. the right-lifts against the left maps). We arrive at the same characterisation of left maps as [4, 7]: The left maps are exactly the strong deformation retracts. In contrast, however, to both, our construction of the factorisation is functorial.

Awodey and Hua [2] give a very general setting in which we can interpret intensional identity types of Martin-Löf type theory: The setting is a category with finite limits, an exponentiable interval $1\rightrightarrows I$, and a universe $𝗍:\dot{𝖳}\to 𝖳$ that is a normal Hurewicz fibration admitting a pullback to its own path type ${\dot{𝖳}}^I\to \dot{𝖳}{\times }_{𝖳}\dot{𝖳}$. In such a category, we generate our WFS from the type families (pullbacks of $𝗍$), by taking the left maps to be left-lifts against the type families, and restricting to the subcategory of types (those objects whose maps to $1$ are type families).

Our construction relies crucially on the fact that each type admits a normal connection $X^I\to {(X^I)}^I$ as constructed in [2], regarded as a strong deformation retraction of the path type $X^I$ onto the type $X$. Following [1, p. 82] and [7, Proposition 6.1.4], we give each map $Y\stackrel{𝑓}{\to }X$ a path object factorisation $Y\to P_f\to X$. This is a variation on Gambino and Garner’s factorisation in [4] through an “identity context”. Unlike their setting, where the factorisation need not be functorial [4, Remark 12], our factorisation through $P_f$ is functorial.

The history of the path object factorisation can be traced back to van den Berg and Garner [7] in a finite limit category, with an abstract path object on an object $X$ playing the role of $X^I$ as in our work. While they assume an internal category structure on the interval, we do not; and while we assume a universe, they do not. Later, van den Berg and Moerdijk [3] show that the factorisation can be performed without requiring the category to have all pullbacks. They do not yield a weak factorisation system because, in their setting, diagonal fillers commute merely up to homotopy. In both our work and in [7], the left maps are the strong deformation retracts. We therefore expect our construction to also be cloven, as in their setting, or even algebraic [6, 5].