The internal Yoneda lemma for locally Cartesian closed $\infty$-categories

Abstract

We formulate and prove internal versions of the Yoneda lemma and of the Yoneda embedding theorem in a finitely complete, locally Cartesian closed $\infty$-category $\mathscr{C}$: for every object $X\in \mathscr{C}$ and every universe $\mathscr{U}$ classifying the diagonal of $X$, the Yoneda map $\mathscr{Y}_X\colon X \to \mathscr{U}^X$ is a monomorphism. The proof uses only finite limits, dependent products and universes, and does not rely on the external Yoneda lemma. The result applies notably to every elementary $\infty$-topos, where it recovers a theorem of Rasekh [Ras18].

Disclosure

“simplicial spaces, [BDGN+16] for parametrized ∞-categories, or [RS17] for synthetic ∞-categories in simplicial type theory. Use of AI assistance. The writing of this paper was assisted by Claude, a large language model made by Anthropic. Mathematically, the AI identified a gap in an earlier version of the proof of Theorem 2.2 (the comparison map induced by よX was not shown to coincide with the equivalence produced by the three mai”

PDF page 3

Classification

Drafting limited passages

Multiplier

5

Verified

2026-08-23T18:54:34.701728Z

Structural counts