rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Improve the proof of naturality of Yoneda lemma in a : A #19

Open fizruk opened 1 year ago

fizruk commented 1 year ago

The proof of naturality of the Yoneda lemma in a : A should be improved to calculate how the covariant family in the domain acts on morphisms f : hom A a b.