Further progress on right orthogonal calculus

[TashiWalde]

1. Right orthogonal maps are closed under composition and right cancel.

2. Right orthogonal maps are closed under relative products (=pullback).

Point 2 was surprisingly tricky. Maybe there was an easier way to do this. I did this by setting up a theory of relative extension types and generalized relative extension types which might be of independent interest.

The two main steps are:

3. A map is right orthogonal if and only if all its relative extension types are contractible if and only if all its generalized relative extension types are contractible.

4. Each relative extension type of the pulled back map appears as retract of a generalized relative extension type of the original map.

Notes:

• Depends on Fiber products #111, where relative products are introduced.
• Partially addresses Formalize closure properties of left orthogonal shapes and right orthogonal maps #81.
• Added a few minor utilities.

[fredrik-bakke]

Okay, I've had enough of making all these formatting corrections, and I'm sure you are done with formatting code and seeing my comments as well. I'll write an autoformatting script over the weekend so we can move on to more productive things.

[fredrik-bakke]

Let me say, although my code comments may not suggest it, I think this PR looks excellent overall.

[TashiWalde]

@fredrik-bakke I have dismissed (marked as resolved) some of your suggestions which should be addressed in the PR #111 on which this one builds.

[fredrik-bakke]

In case you missed it, there's a single comment left to resolve. After that, this PR seems ready to merge to me.

[fredrik-bakke]

Okay, I've had enough of making all these formatting corrections, and I'm sure you are done with formatting code and seeing my comments as well. I'll write an autoformatting script over the weekend so we can move on to more productive things.

I had a chat with Nikolai before the weekend. He and his student will try to set up basic autoformatting functionality built into the Rzk ecosystem instead, so the autoformatting will have to wait a little.