Category theorist extends Yoneda Lemma to double categories without presheaves
A category theory writeup describes how to construct a Yoneda-style embedding within double categories, a setting where presheaves cannot be directly expressed because objects are treated as abstract 0-cells rather than sets. The author sketches how to define a presheaf object and a Yoneda vertical arrow using universal constructions like horizontal arrows and left Kan extensions instead of direct references to sets or presheaves. A follow-up post is promised that will implement these ideas as working code in Haskell.