Abstract We study exponentiable functors in the context of synthetic $\infty$ -categories. We do this within the framework of simplicial homotopy type theory of Riehl and Shulman. Our main result characterizes exponentiable functors. In order to achieve this, we explore Segal type completions. Moreover, we verify that our result is semantically sound.

Abstract We develop the theory of limits and colimits in $\infty$ -categories within the synthetic framework of simplicial homotopy type theory established by Riehl and Shulman. We also show that in this setting, the limit of a family of spaces can be computed as a dependent product.