Homotopy Type Theory
representable functor (Rev #1)

Idea

Definition

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

Properties

Theorem 9.5.9

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

Proof. By definition “F is representable” is just the fiber of y 0\mathbf{y}_0 over FF. Since y 0\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

Revision on October 8, 2018 at 17:44:44 by Ali Caglayan. See the history of this page for a list of all contributions to it.