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:

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

[jonweinb]

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