Formalize strict adjoint sections, LARI families and its closure properties

[TashiWalde]

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...

[TashiWalde]

Let me also repeat here what I already announced on Zulip. My Master student Benno Lossin has formalized a lot of material regarding LARI-orthogonality.

We will hopefully be able to start with the merging process soon. Meanwhile you can check out his code on his public sHoTT-fork: https://github.com/BennoLossin/sHoTT

(This might be of particular interest to @jonweinb and @emilyriehl .)

[emilyriehl]

Oh great! Congrats to Benno and we'll look forward to having this in the library. Please tag us when you start the PRs to make sure we see it right away.