A functor is said to be representable if there exists and an isomorphism? .
If is a category, then the type “F is representable” is a mere proposition.
Proof. By definition “F is representable” is just the fiber of over . Since is an ambedding by Corollary 9.5.7 (see Yoneda lemma), this fiber is a mere proposition.
Category theory functor Yoneda lemma
Revision on October 11, 2018 at 10:29:57 by Ali Caglayan. See the history of this page for a list of all contributions to it.