Formalize strict adjoint sections, LARI families and its closure properties

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

44 stars 12 forks source link

Formalize strict adjoint sections, LARI families and its closure properties #133

Open TashiWalde opened 1 year ago

TashiWalde commented 1 year ago

Now that the formalization of right orthogonality and its closure properties is well underway (#81), it is time to start the analogous story for LARI/RARI-orthogonality.

[ ] Formalize strict left and right adjoint sections / reflectors / coreflectors / LARI/RARI - maps.
[ ] Formalize the corresponding notion of orthogonality.
[ ] Formalize closure properties...