Formalise discrete fibers (Section 8.4 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

Formalise discrete fibers (Section 8.4 of RS17 paper) #15

Open fizruk opened 1 year ago

fizruk commented 1 year ago

All of these should be straightforward.

[ ] Proposition 8.18
[ ] Corollary 8.19
[ ] Corollary 8.20

emilyriehl commented 1 year ago

@nimarasekh is going to need this fairly soon. Any new contributors want to give Proposition 8.18 a try? I'm happy to help give pointers to results in the library that would help.

emilyriehl commented 1 year ago

@stiephenpradal is going to work on this.