AI 中文总结
在有限完备、局部笛卡尔闭的∞-范畴\(\C\)中阐述并证明约当引理等的内部版本，证明仅用有限极限等，不依赖外部约当引理，并应用于初等∞-拓扑斯，恢复相关定理。
AI 中文摘要
我们在有限完备、局部笛卡尔闭的∞-范畴\(\C\)中阐述并证明了约当引理和约当嵌入定理的内部版本：对于\(\C\)中每个对象\(X\)以及对\(X\)的对角线进行分类的每个全域\(\U\)，约当映射\(\yo_X\colon X\to\U^X\)是单态射。证明仅使用有限极限、依赖积和全域，不依赖外部约当引理。该结果特别适用于每个初等∞-拓扑斯，恢复了拉塞克的一个定理。
英文摘要
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].
Comments15 pages, comments welcome! v2: added an application to higher covering spaces, the original motivation for this work
