search

rzk-lang / sHoTT

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

Discrete fibers #99

Closed StiephenPradal closed 1 year ago

StiephenPradal commented 1 year ago

Hi, Here are Proposition 8.18 and Corollary 8.19 from the Discrete Fibers section. I'm not 100% sure about the terminology and type-setting conventions, let me know if there is anything to change.

emilyriehl commented 1 year ago

Overall this looks very good. I just made a few minor nitpicks. Then this is ready to merge.

Note we're in the process of updating the style guide but right now let's follow the past conventions.