## Idea ## ## Definition ## 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$ ## See also ## [[Category theory]] [[functor]] [[Yoneda lemma]] ## References ## [[HoTT book]] category: category theory