Stable factorization from a fibred algebraic weak factorization system

2019/10/07 by Cavallo, Evan
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO)

paper · doi:10.48550/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.

Related

• A category-theoretic version of the identity type weak factorization system
• Type-theoretic weak factorization systems
• Kripke-Joyal forcing for type theory and uniform fibrations
• The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems
• Identity Types in Algebraic Model Structures and Cubical Sets