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

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 $\C$: for every object $X\in\C$ and every universe $\U$ classifying the diagonal of $X$, the Yoneda map $\yo_X\colon X\to\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 \cite{Rasekh_YonedaLemmaElementaryTopos}.