Higher Structures, Vol. 7, No. 1, pp. 74-165, 2023
Synthetic fibered (∞,1)-category theory
Jonathan Weinberger, Ulrik Buchholtz
Received May 4th 2021. Published online May 21st 2023.
Abstract: We study cocartesian fibrations in the setting of the synthetic (∞,1)-category theory developed in simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations.
Keywords: homotopy type theory; simplicial type theory; (∞; 1)-categories; Segal spaces; Rezk spaces; cartesian fibrations