Stable factorization from a fibred algebraic weak factorization system
Category Theory
2019-11-20 v2 Logic in Computer Science
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.
Cite
@article{arxiv.1910.03121,
title = {Stable factorization from a fibred algebraic weak factorization system},
author = {Evan Cavallo},
journal= {arXiv preprint arXiv:1910.03121},
year = {2019}
}
Comments
11 pages. v2: correct typos