5 - Presheaves: Internally

Summary

The aim of this chapter is to construct the ∞-category of small ∞-groupoids, as well as the Hom functor of a locally small ∞-category. We introduce a very general theory of minimal fibrations which we use to construct the universal left fibration. We prove that this universal fibration is univalent, which means that it is indeed universal in a homotopy-theoretic way. The codomain of the universal left fibration is, by definition, the ∞-category of small ∞-groupoids. We examine the relationship between the covariant model categories and the category of functors with values in the ∞-category of small ∞-groupoids. We introduce the twisted arrow ∞-category as the diagonal of a bisimplicial set, and study a bivariant version of the covariant model structure for this to make sense. This in turn is used to define the Yoneda embedding. We introduce and discuss the notion of locally small ∞-category. We finally prove the internal version of the Yoneda lemma, which is a fully functorial version in the sense of higher category theory.