Formalise representable functors (Proposition 9.10 of RS17 paper)

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

44 stars 12 forks source link

Closed fizruk closed 3 weeks ago

fizruk commented 1 year ago

Should be fairly straightforward, following the proof in the paper.

jonalfcam commented 1 year ago

If no one has gone after this yet, I will.