Further progress on right orthogonal calculus - part 2 - Githubissues

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

https://rzk-lang.github.io/sHoTT/

44 stars 12 forks source link

Further progress on right orthogonal calculus - part 2 #118

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Equivalences are right orthogonal to every shape inclusion
Right orthogonal maps are closed under equivalence
Weak version of left cancel with section

Partially addresses #81.