A functor$F: \mathit{Set}^{A^{op}}$ is said to be representable if there exists $a:A$ and an isomorphism?$\mathbf{y}a \cong F$.

Properties

Theorem 9.5.9

If $A$ is a category, then the type “F is representable” is a mere proposition.

Proof. By definition “F is representable” is just the fiber of $\mathbf{y}_0$ over $F$. Since $\mathbf{y}_0$ is an ambedding by Corollary 9.5.7 (see Yoneda lemma), this fiber is a mere proposition. $\square$