Generalized Chevalley criteria in simplicial homotopy type theory

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