rzk-lang / sHoTT

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

Fiber products #111

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Introduce fiber-products of maps B -> A <- C in two ways:

Show that these two constructions agree.