Exponentiable functors between synthetic $\infty$-categories

TL;DR

This paper characterizes exponentiable functors within synthetic ∞-categories using simplicial Homotopy Type Theory, providing a semantic verification and exploring Segal type completions to deepen the understanding of these functors.

Contribution

It offers a new characterization of exponentiable functors in synthetic ∞-categories within the framework of simplicial Homotopy Type Theory, including semantic validation.

Findings

Characterization of exponentiable functors in synthetic ∞-categories

Semantic soundness of the main results verified

Exploration of Segal type completions

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.