search

rzk-lang / sHoTT

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

More functoriality of fibers #134

Closed TashiWalde closed 12 months ago

TashiWalde commented 1 year ago

Deduce that retracts of equivalences are equivalences.

I have introduced the universe of maps (called Map) in 00-common. Please let me know if this is supposed to be elsewhere.