rzk-lang / sHoTT

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

Preservation of fibers under equivalences #106

Closed aergus closed 1 year ago

aergus commented 1 year ago

Here is a formalization of a fact @emilyriehl suggested on Zulip.

If a more explicit comparison map between the fibers is desirable, I could try to prove the "functoriality" of the fiber w.r.t. maps between domains and derive this fact from that.