  We study cocartesian fibrations in the setting of the synthetic
$(\infty,1)$-category theory developed in the simplicial type theory introduced
by Riehl and Shulman. Our development culminates in a Yoneda Lemma for
cocartesian fibrations.

Category Theory;Logic in Computer Science;Algebraic Topology;Logic