search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

Yoneda rearrangement #4

Closed jonsterling closed 7 years ago

jonsterling commented 7 years ago

The "Yoneda Lemma" is usually understood as the statement about presheaves (contravariant functors); the one about copresheaves is, I think, just called the "covariant Yoneda lemma".

The "Coyoneda lemma" states that every presheaf is a colimit of representables. This would be interesting to prove as well!

I hope you don't mind these changes!

jwiegley commented 7 years ago

I'd like to get to colimits and representables fairly soon, so I'll add a TODO note to prove this connection to Yoneda.