Cotruncated morphisms form a modality

We start by showing that \((L,L^{\perp})\) is a factorization system. In light of Proposition A.11, it suffices to show that \(L\) is saturated and of small generation.Let \(\nabla\colon \Ar(T)\to\Ar(T)\) be the codiagonal functor, which sends \(f\colon X\to Y\) to \(\nabla_f\colon Y\sqcup_XY\to Y\). This is an accessible functor, since it is constructed from finite colimits. By Definition 5.5, a morphism \(f\) is \(n\)-cotruncated if and only if \(\nabla^{n+2}(f)\) is an isomorphism. Consequently, \(L\) is the inverse image under the accessible functor \(\nabla^{n+2}\) of the accessible subcategory of isomorphisms in \(\Ar(T)\). It follows that \(L\subseteq\Ar(T)\) is accessible and accessibly embedded.The class \(L\) is saturated. Indeed, this is immediate for \(n=-2\), and the inductive step follows because the codiagonal construction preserves colimits in \(\Ar(T)\). Since \(L\) is accessible, accessibly embedded, and closed under all colimits, it is generated under colimits by a small collection of its objects. In particular, it is the saturation of a small set of morphisms.To show that the \(n\)-cotruncated maps are stable under base change, consider a pullback square

and assume that \(f\) is \(n\)-cotruncated. We will show that also \(f'\) is \(n\)-cotruncated. By induction, it will suffice to show that the following square is a pullback square:

But this is clear from universality of colimits.