Stable factorization from a fibred algebraic weak factorization system

TL;DR

This paper introduces a new method for constructing stable diagonal factorizations in categories, facilitating models of type theory with identity types, inspired by cubical type theory and algebraic weak factorization systems.

Contribution

It provides a novel construction of stable diagonal factorizations from algebraic weak factorization systems, offering an alternative approach to modeling identity types in categorical type theory.

Findings

Constructs stable diagonal factorizations from algebraic weak factorization systems.

Offers a new categorical model for type theory with identity types.

Provides an alternative to existing models inspired by cubical type theory.

Abstract

We present a construction of stable diagonal factorizations, used to define categorical models of type theory with identity types, from a family of algebraic weak factorization systems on the slices of a category. Inspired by a computational interpretation of indexed inductive types in cubical type theory due to Cavallo and Harper, it can be read as a refactoring of a construction of van den Berg and Garner, and is a new alternative among a variety of approaches to modeling identity types in the literature.