Homotopy Type Theory
representable functor



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.


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


Yoneda lemma


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.