Generalized Chevalley criteria in simplicial homotopy type theory

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 $(\infty ,1)$-category theory.

19 pages. This text is based on Appendix A from author's PhD thesis arXiv:2202.13132. Comments welcome!