search

rzk-lang / sHoTT

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

functorial instance of cofibration-composition #79

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

1) Define the type of equivalences between equivalences.

2) Show that cofibration-composition is functorial in the sense that for each A' -> A it induces an equivalence of maps.

3) Show that cofibration-union is functorial.

emilyriehl commented 1 year ago

@TashiWalde I think I've put the functorial retract stuff where you wanted it to appear in the file but please double check. I'll go ahead and merge. If I messed something up, let me know and I can fix it.