search

rzk-lang / sHoTT

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

Formalize yoneda embedding #100

Closed cesarbm03 closed 1 year ago

cesarbm03 commented 1 year ago

Definition 9.3 and Remark 9.4 of RS17

cesarbm03 commented 1 year ago

Thank you for your observations, I'll make the changes you have pointed out.

cesarbm03 commented 1 year ago

Hi @emilyriehl, @fizruk and @jonweinb. I have made the requested changes and I think this is ready for review.

emilyriehl commented 1 year ago

@cesarbm03 sorry to be so slow to get back to this. Your later PR formalize-yoneda-embedding-2 was merged, correct? So should this PR just be deleted? If I recall correctly those changes subsumed these ones.

cesarbm03 commented 1 year ago

No worries at all! #103 was merged into this PR. This PR goes to main, it is the one that includes the full proof and implements all the comments.

emilyriehl commented 1 year ago

Thanks @cesarbm03 for clarifying. There were a couple other term name changes we discussed. Would you mind if I implemented them?

cesarbm03 commented 1 year ago

Not at all! I did change some, but I must have missed others. Make the implementations as you see appropriate.

De : Emily Riehl @.> Envoyé : Saturday, October 21, 2023 11:11:18 PM À : rzk-lang/sHoTT @.> Cc : Cesar Bardomiano Martinez @.>; Mention @.> Objet : Re: [rzk-lang/sHoTT] Formalize yoneda embedding (PR #100)

Attention : courriel externe | external email

Thanks @cesarbm03https://github.com/cesarbm03 for clarifying. There were a couple other term name changes we discussed. Would you mind if I implemented them?

— Reply to this email directly, view it on GitHubhttps://github.com/rzk-lang/sHoTT/pull/100#issuecomment-1773979943, or unsubscribehttps://github.com/notifications/unsubscribe-auth/BCWX4GXMMUIRKDBIIWBH4OLYASFFNAVCNFSM6AAAAAA5Y67Q4GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONZTHE3TSOJUGM. You are receiving this because you were mentioned.Message ID: @.***>

emilyriehl commented 1 year ago

Actually it all looks good. Merging now.

cesarbm03 commented 1 year ago

Thank you!