Added a proof of the naturality of the equivalence of the Yoneda lemma in the covariant family.
The proof of the naturality of the equivalence of the Yoneda lemma in the represented object will follow formally once we've shown that the domain of evid is a covariant family over A (but this is a bit involved to prove).
In parallel, some formatting improvements were implemented throughout the covariant families file, which hadn't yet been updated.
Added a proof of the naturality of the equivalence of the Yoneda lemma in the covariant family.
The proof of the naturality of the equivalence of the Yoneda lemma in the represented object will follow formally once we've shown that the domain of evid is a covariant family over A (but this is a bit involved to prove).
In parallel, some formatting improvements were implemented throughout the covariant families file, which hadn't yet been updated.