search

rzk-lang / sHoTT

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

Functorial shape retract #67

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Introduce a convenient way to state that a shape inclusion \phi \subset \psi is a retract functorially, for example \Delta^2 \subset \Delta^1\times\Delta^1.

Relies on #59.

emilyriehl commented 1 year ago

@TashiWalde this is nice. I just added a short paragraph above your definition because it took me a while to understand it. Feel free to tweak what I've written in a future PR if you'd like to improve the text.