A Proof of Covariant Yoneda Lemma in the Lean3 Proof Assistant out of scratch not using Mathlib3. This proof was first constructed in my teaching Introduction to Proofs to upper Level undergraduates at Johns Hopkins University.
sinhp/CovariantYonedaLean3
A Proof of Covariant Yoneda Lemma in the Lean3 Proof Assistant out of scratch not using Mathlib3.
LeanMIT