# Homotopy Type Theory representable functor

## 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$

Category theory

functor

Yoneda lemma

## References

HoTT book

category: category theory

Last revised on October 11, 2018 at 06:29:57. See the history of this page for a list of all contributions to it.