HoTT/HoTT — pull request #307 by JasonGross (2014-01-18 01:03:06+00:00)
Title: Port the yoneda lemma from catdb

I strongly suspect it can be generalized (as a first step, I think that I only presented the morphism parts of the natural transformations). Is there a version of the Yoneda lemma that subsumes the covariant and contravariant versions (and talks about the hom functor `Cᵒᵖ × C → Set`, rather than about a partially applied hom functor)?