Stable factorization from a fibred algebraic weak factorization system
arXiv:1910.03121
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.
11 pages. v2: correct typos
References in corpus (8)
- The identity type weak factorisation system
- Algebraic model structures
- Axioms for Modelling Cubical Type Theory in a Topos
- Towards a constructive simplicial model of Univalent Foundations
- The Equivalence Extension Property and Model Structures
- W-Types with Reductions and the Small Object Argument
- Lifting Problems in Grothendieck Fibrations
- Identity Types in Algebraic Model Structures and Cubical Sets