A category-theoretic version of the identity type weak factorization system

TL;DR

This paper generalizes the concept of identity type weak factorization systems using category theory, extending previous results to a broader class of models including topological and simplicial ones.

Contribution

It introduces a category-theoretic framework called a tribe with weakly stable path objects, generalizing Gambino and Garner's weak factorization system for identity types.

Findings

Established a purely category-theoretic version of the identity type weak factorization system.

Unified the weak factorization systems from topological and simplicial models.

Extended the applicability of identity type structures in categorical settings.

Abstract

Gambino and Garner proved that the syntactic category of a dependent type theory with identity types can be endowed with a weak factorization system structure, called identity type weak factorization system. In this paper we consider an enrichment of Joyal's notion of tribe, which we call a tribe with weakly stable path objects, and prove a purely category-theoretic version of the identity type weak factorization system, thus generalizing Gambino and Garner's result. We conclude showing that this structure subsumes also the weak factorization systems coming from the topological and simplicial models of identity types obtained by van den Berg and Garner.