Equivalences of maps induce equivalences of fibers

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

44 stars 12 forks source link

Closed aergus closed 1 year ago

aergus commented 1 year ago

@TashiWalde said that he needs this.

TashiWalde commented 1 year ago

Thanks for implementing this!

emilyriehl commented 1 year ago

Looks great.