Basic properties of orthogonal maps

[fredrik-bakke]

• Coproducts of pullbacks are pullbacks
• Gives some equivalent characterizations of orthogonal maps
• Orthogonal maps are closed under homotopy
• Equivalences are left and right orthogonal to any map
• Right orthogonal maps are closed under
  • Composition
  • Left cancellation
  • Dependent products
  • Postcomp exponentiation
  • Products
  • Base change
• Left orthogonal maps are closed under
  • Composition
  • Right cancellation
  • Dependent sums
  • Coproducts
• Local (dependent) types are closed under
  • equivalent types
  • function homotopy
• A type is f-local if and only if its terminal map is
• A type is f-local if and only if its terminal map is f-orthogonal
• A dependent type is f-local if its fibers are f-null
• Code formatting and refactoring for pullbacks and miscellaneous.

[fredrik-bakke]

I'm just posting this PR now to announce what I'm working on to ensure we don't double up work, but I don't have a clear endpoint in mind for it yet.

[fredrik-bakke]

Since I don't know when I will be able to continue working on this, I will mark it as ready for review now. I think this is a reasonable ending point anyway.

[fredrik-bakke]

The type checker ran out of memory again 😬

[fredrik-bakke]

Since I don't know when I will be able to continue working on this, I will mark it as ready for review now. I think this is a reasonable ending point anyway.

Actually. I take that back. There are things I want to change that are added in this PR. It would be unfair to make you review it when I want to change it later anyway. I'll let this PR stand until I have time to complete it.

[EgbertRijke]

Excellent work! Thank you for all the improvements throughout the library, and the many new additions!

[fredrik-bakke]

Whenever you write vertical-cone or horizontal-cone in a name, wouldn't it be better to write vertical-map-cone and horizontal-map-cone? Or do you really mean to suggest that these names are about vertical and horizontal cones?

I think I originally intended the word vertical to bind to whatever is left of it. I.e. parse map-fiber-vertical-cone as (map-fiber-vertical)-cone. I'm okay with changing it to have an extra map- if you prefer.

[fredrik-bakke]

Thank you for the nice review and encouraging comments! I really appreciate it ❤️

[EgbertRijke]

If you could change vertical-cone to vertical-map-cone and horizontal-cone to horizontal-map-cone then I think this PR could be merged

[EgbertRijke]

In #885 I am changing the horizontal/vertical terminology for cocones to left/right, however, because it was creating some frictions and some unsensible naming in some instances. So please note that while I'm ok with merging this PR which extends the horizontal/vertical scheme, I will propose to change it later. It is still beneficial though, that you're introducing the scheme here, because it makes it easier to change to left/right.

[fredrik-bakke]

Great, thanks! I'll see if I can get it done tomorrow.

[fredrik-bakke]

There you go!