Generalized Chevalley criteria in simplicial homotopy type theory
Category Theory
2024-03-14 v1 Logic in Computer Science
Algebraic Topology
Logic
Abstract
We provide a generalized treatment of (co)cartesian arrows, fibrations, and functors. Compared to the classical conditions, the endpoint inclusions get replaced by arbitrary shape inclusions. Our framework is Riehl--Shulman's simplicial homotopy type theory which supports the development of synthetic internal -category theory.
Keywords
Cite
@article{arxiv.2403.08190,
title = {Generalized Chevalley criteria in simplicial homotopy type theory},
author = {Jonathan Weinberger},
journal= {arXiv preprint arXiv:2403.08190},
year = {2024}
}
Comments
19 pages. This text is based on Appendix A from author's PhD thesis arXiv:2202.13132. Comments welcome!