Formalise the Yoneda embedding (Definition 9.3 and Remark 9.4 of RS17 paper) - Githubissues

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

https://rzk-lang.github.io/sHoTT/

44 stars 12 forks source link

Formalise the Yoneda embedding (Definition 9.3 and Remark 9.4 of RS17 paper) #20

Closed fizruk closed 11 months ago

fizruk commented 1 year ago

[ ] Definition 9.3
[ ] Remark 9.4

cesarbm03 commented 11 months ago

I am closing this via #100.