Formalize closure properties of left orthogonal shapes and right orthogonal maps

[TashiWalde]

The notion of orthogonality from BW23 is formalized in #76.

It satisfies many desirable closure properties:

• [x] In the left argument:
  • [x] isomorphism of shape-pairs
  • [x] composition
  • [x] left cancellation
  • [x] right cancellation with retraction
  • [x] pushout product
  • [x] crossing with a shape
  • [x] exact pushout
  • [x] retracts
• [ ] in the right argument:
  • [x] equivalence of maps
  • [x] composition
  • [x] right cancellation
  • [x] left cancellation with section
  • [x] exponentiation
  • [x] pullback
  • [ ] retracts
• [ ] and many more

[jonweinb]

Great, thanks a lot @TashiWalde for taking the initiative on this!