arXiv · 1910.03121
Stable factorization from a fibred algebraic weak factorization system
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.
Explore related subjects
Keep this discovery
Evan Cavallo. 2019-10-07. Stable factorization from a fibred algebraic weak factorization system. https://arxiv.org/abs/1910.03121
Cite the original work for its findings. Save a collection to share your selection of sources.