We set up a set theory axiomatically by fixing certain statements about "$\in$". There are many different set theories. The Yoneda lemma (the theorem about functors to Set) is a early but central result in category theory and relates very much to sets (the functor is to Set, and often the Hom-sets are indeed sets and the collection of natural transformations.)

Now if you pull up category theory, maybe in purely logical terms, or within a type theoretic background, or maybe using some small set theory, then you will somehow get to some variant of the Yoneda lemma and indirectly say something about sets.

My question is: What is the least restrictive notion of "set" so that we can justify to say the Yoneda indeed tells us something about sets or embeddings in "the world of sets"? For exmaple, I hardly imagine we need to assume the axiom schema of replacement to end up with the Yoneda lemma, but conversely I expect the "sets" talked about in the Yoneda lemma must be subject of some sort of comprehension principle.

  • $\begingroup$ You don't need very much comprehension, because we're not really forming any new sets. But we do need to be able to define maps. Replacement can be avoided provided you have disjoint unions of certain sets. $\endgroup$
    – Zhen Lin
    Commented Mar 27, 2014 at 14:43

1 Answer 1


[EDIT: I miscalculated local exponents in the previous revision of this answer. Local cartesian closedness is, obviously, unnecessary.]

We have a Yoneda lemma whenever we can speak of categories relative to any "sets" that form a category. In particular, it suffices that the category of "sets" has pullbacks. If $\mathbb{C}$ has pullbacks, then for every category $A$ internal to $\mathbb{C}$ there is a full and faithful functor:

$$y_A \colon A \rightarrow \mathbb{C}^{A^{op}}$$

where $\mathbb{C}^{A^{op}}$ is thought of as a locally $\mathbb{C}$-internal category of internal presheaves on $A$, and $y_A$ is the adjoint transposition of:

$$\hom(=, -) \colon A^{op} \times A \rightarrow \mathbb{C}$$

which is defined on generalized objects $X, Y \in_K A$ as the local exponent $X^Y$. In more details, let $X, Y \colon K \rightarrow A_0$ be two morphisms in $\mathbb{C}$ (i.e. objects in the fibre over $K$ in the externalisation of $A$), where $A_0$ is the object of objects of category $A$. The local exponent $X^Y$ is defined as the representation of:

$$K' \overset{f}\rightarrow K \mapsto \hom_{\mathbf{Cat}(\mathbb{C})}(K', A)(X \circ f, Y \circ f)$$

Morphisms $X \circ f \rightarrow Y \circ f$ in $\hom_{\mathbf{Cat}(\mathbb{C})}(K', A)$ are internal natural transformations. Spelling out the definition, we have a morphism $\alpha \colon K' \rightarrow A_1$ in $\mathbb{C}$ that commutes with $X \circ f$ and $Y \circ f$ --- i.e. $X \circ f = \mathit{dom} \circ \alpha$ and $Y \circ f = \mathit{cod} \circ \alpha$, where $\mathit{dom}, \mathit{cod} \colon A_1 \rightarrow A_0$ are the usual projections from objects of morphisms $A_1$ to the object of objects $A_0$. In other words: $$\langle X, Y \rangle \circ f = \langle \mathit{dom}, \mathit{cod} \rangle \circ \alpha$$ and for given $f$, morphisms $\alpha$ are tantamount to morphisms to the pullback of $\langle X, Y \rangle$ with $\langle \mathit{dom}, \mathit{cod} \rangle$, which we denote by $\hom(X, Y)$. By the universal property of pullbacks, this operation extends to the locally internal functor $A^{op} \times A \rightarrow \mathbb{C}$.

Moreover, if $\mathbb{C}$ has finite colimits and is additionally locally cartesian closed, then $\mathbb{C}^{A^{op}}$ is an internal monoidal free (small) cocompletion of $A$. See also this question on MO:



You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .