Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exponentiable functors between synthetic $\infty$-categories

César Bardomiano-Martínez

TL;DR

This work develops a synthetic theory of exponentiable functors between $(\infty,1)$-categories inside $sHoTT$, introducing Segal type completion as a universal way to complete a type to a Segal type and proving a Conduché-style criterion for exponentiability at the Segal-type level. It specializes the criterion to Rezk types and demonstrates semantic alignment with the standard bisimplicial-set model, establishing soundness of the synthetic definitions. The paper also connects exponentiable functors to profunctor composition via a coend-like construction and discusses the limits of encoding correspondences in $sHoTT$, identifying directions for future refinement. Overall, it provides a foundational framework for internal exponentiation in synthetic higher category theory and links these notions to established $\infty$-categorical results.

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.

Exponentiable functors between synthetic $\infty$-categories

TL;DR

This work develops a synthetic theory of exponentiable functors between -categories inside , introducing Segal type completion as a universal way to complete a type to a Segal type and proving a Conduché-style criterion for exponentiability at the Segal-type level. It specializes the criterion to Rezk types and demonstrates semantic alignment with the standard bisimplicial-set model, establishing soundness of the synthetic definitions. The paper also connects exponentiable functors to profunctor composition via a coend-like construction and discusses the limits of encoding correspondences in , identifying directions for future refinement. Overall, it provides a foundational framework for internal exponentiation in synthetic higher category theory and links these notions to established -categorical results.

Abstract

We study exponentiable functors in the context of synthetic -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.
Paper Structure (10 sections, 11 theorems, 62 equations)

This paper contains 10 sections, 11 theorems, 62 equations.

Table of Contents

  1. Introduction
  2. Synthetic $\infty$-category theory
  3. Exponentiable functors
  4. Outline
  5. The Segal type completion
  6. Conduché's theorem
  7. The bisimplicial sets semantics of sHoTT
  8. Segal type completion and Segal space completion
  9. Exponentiable functors
  10. On profunctors and correspondences

Key Result

Theorem 1.1

For a functor $f:\mathcal{E} \to \mathcal{B}$, the following conditions are equivalent:

Theorems & Definitions (29)

  • Theorem 1.1
  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Proposition 2.6
  • proof
  • Proposition 3.1
  • Theorem 3.2
  • ...and 19 more