A categorical model structure for generalized algebraic theories
Abstract
We describe a (combinatorial, monoidal, Cat-enriched) Quillen model structure on the category of Cartmell's generalized algebraic theories (gats); its homotopy bicategory consists essentially of Taylor's rooted display map categories. This allows us to compare two kinds of morphisms of gats: one where sort dependency and substitution are preserved strictly, thus directly matching the syntax, and one where the given structure is preserved up to isomorphism. We prove a strictification result for morphisms out of cofibrant theories, which are the retracts of theories without sort equality axioms. Along the way, we give a structural characterization of when a contextual category can be presented without sort equality axioms. Our results also imply that when restricted to cofibrant objects, the tensor product of gats has the expected semantic behaviour, namely, it corresponds to the tensor product of locally finitely presentable categories equipped with a cofibrantly generated weak factorization system. Strict and weak morphisms specialize, respectively, to two familiar concepts of model of a gat A: ones valued in iterated families of sets, with substitution interpreted as reindexing, and set-valued models of the contextual category C(A) viewed as a finite-limit sketch. We characterize strictifiability of a model of the latter kind via a loop freeness condition on a certain map of functors out of the category of context projections of A.
Related
- Harmonic torsion of algebraic generalized Ricci solitons and the structure of solvable extensions
- Duality theory for categorical theories
- A higher categorical approach to graded bivariant K-theories for Real C*-algebras
- A characterization of the finite model property for ω-categorical theories
- Categorical representations of algebraic groups in positive characteristic
BibTeX
@misc{almeida2026categorical,
title = {{A categorical model structure for generalized algebraic theories}},
author = {Daniel Almeida},
howpublished = {arXiv},
year = {2026},
month = aug,
doi = {10.48550/arxiv.2608.27667},
eprint = {2608.27667},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.27667},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A categorical model structure for generalized algebraic theories
AU - Daniel Almeida
PY - 2026
DA - 2026/08/27
PB - arXiv
DO - 10.48550/arxiv.2608.27667
UR - https://arxiv.org/abs/2608.27667
AB - We describe a (combinatorial, monoidal, Cat-enriched) Quillen model structure on the category of Cartmell's generalized algebraic theories (gats); its homotopy bicategory consists essentially of Taylor's rooted display map categories. This allows us to compare two kinds of morphisms of gats: one where sort dependency and substitution are preserved strictly, thus directly matching the syntax, and one where the given structure is preserved up to isomorphism. We prove a strictification result for morphisms out of cofibrant theories, which are the retracts of theories without sort equality axioms. Along the way, we give a structural characterization of when a contextual category can be presented without sort equality axioms. Our results also imply that when restricted to cofibrant objects, the tensor product of gats has the expected semantic behaviour, namely, it corresponds to the tensor product of locally finitely presentable categories equipped with a cofibrantly generated weak factorization system. Strict and weak morphisms specialize, respectively, to two familiar concepts of model of a gat A: ones valued in iterated families of sets, with substitution interpreted as reindexing, and set-valued models of the contextual category C(A) viewed as a finite-limit sketch. We characterize strictifiability of a model of the latter kind via a loop freeness condition on a certain map of functors out of the category of context projections of A.
ER -