If a locally cartesian closed category carries a weak factorization system, then the left maps are stable under pullback along right maps if and only if the right maps are closed under pushforward along right maps. In this paper we state and prove an analogous result for algebraic weak factorization systems. These algebraic weak factorization systems are an explicit variant of the more traditional weak factorization systems in that the factorization and the lifts are part of the structure of an algebraic weak factorization system and are not merely required to exist. Our work has been motivated by the categorical semantics of type theory, where the closure of right maps under pushforward provides a useful tool for modelling dependent function types. We illustrate our ideas using split fibrations of groupoids, which are the backbone of the groupoid model of Hofmann and Streicher.
Keywords: Algebraic weak factorization systems, Double categories, Categorical semantics of type theory
2020 MSC: 18A32, 18N10, 18N45
Theory and Applications of Categories, Vol. 45, 2026, No. 5, pp 176-205.
Published 2026-01-20.
TAC Home