Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
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. – Zhen Lin Mar 27 '14 at 14:43

[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:

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.