Homotopy Type Theory representable functor > history (Rev #3, changes)

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