Refactoring of retractions, sections, and equivalences, and adding the 6-for-2 property of equivalences

[EgbertRijke]

• Some cleanup of the commuting-triangles-of-maps file. I moved the commuting triangles induced by sections and retractions here, and moved the action of precomposition on commuting traingles to functoriality-of-function-types
• A total cleanup of foundation-core.equivalences. One of the ways I cleaned up was by writing a bit more infrastructure for sections and retractions. This made the long names obsolete, because now the projections are named. This is also a general case I would like to make against long variable names: If you write proper infrastructure then you don't need long variable names, plus it will be a lot easier to maintain your naming scheme and not float off course with it.
• The foundation-core.equivalences file now contains much more explanations.
• I introduced a new naming scheme for proving that certain maps in commuting triangles have certain properties. Previously we had parts of names like left-factor-htpy, which was supposed to mean the left factor up to homotopy. However, I think it is clearer if we mention triangle in such names, and name the map in the triangle that is the subject of the assertion. Note that diagrammatic ordering is usually the opposite of the compositional ordering, so left-factor-htpy got replaced by right-map-triangle. Similarly, I replaced comp-htpy by left-map-triangle and right-factor-htpy by top-map-triangle. This change triggered a lot of changes throughout the library.
• I added names for the projections out of the fiber of a map. We failed to do so previously, and it lead to clumsy formalization in some places. There are probably other places in the library where we could use those names, but I didn't go look for them as it would trigger another lot of changes throughout many files.
• In retractions I added a predicate for is-retraction, for obvious reasons
• In sections I added a predicate for is-section. In both cases I could have gone through the library and implement this predicate throughout. I didn't do so, but I could potentially do that in a subsequent pull request (not this one).
• I factored out retracts-of-types from retractions, because it is a separate concept from the concept of a retraction of a map, even though it is of course closely related. One thing I did in this file was introduce a non-infix notation for retracts of types. We usually have some non-infix notation for infix operators that indicate how to use statements involving that operator in a naming scheme. Writing retract-of in names quickly looks very awkward, so I improved that to retract using this setup.
• I moved the file retracts-of-maps from orthogonal-factorization-systems to foundation, so that it can be next to retracts-of-types
• I worked the new infrastructure into the file retracts-of-maps, but that triggered lots of changes throughout that file. I ended up renaming quite a lot of things, and I hope that is ok. One of the thing I fixed was that the word section was used in names, but no element of section _ was constructed or involved. I also replaced retract-of-map with retract-map to not have to write of so often. Prepositions are not very common in our naming scheme, and I think our naming scheme is better when we use them very sparingly.

[VojtechStep]

I'm leaving a partial review for now. So far I like the changes, especially the renaming of 3-for-2 up to homotopies, I could never remember which one is which 👌

[fredrik-bakke]

Thanks for fixing up the retracts-of-maps file for me! (I only reviewed that one for now)

[EgbertRijke]

I made some simplifications to the proof that retracts of equivalences are equivalences. In particular, I avoided all explicit constructions of homotopies, since they were all consequences of things that were already constructed in the library.

[fredrik-bakke]

Thanks for simplifying the proofs! It originally went from an observation that the higher coherence assumed in the HoTT-UF book wasn't needed to what I submitted in my previous PR, so in the end I didn't consider looking for an even simpler proof. I'm glad you still kept them around though, as I think they're still instructive to have there

[EgbertRijke]

I think it is exactly the same proof as the one you gave, except it is packaged up in terms of earlier constructions in the library. I probably wouldn't have thought of it if you hadn't already simplified the proof.

Now I would still like to think about that identification that you earlier marked abstract. It would be nice to have an informal explanation of that construction, because it is hard to understand just by looking at the code.

[fredrik-bakke]

Oh, you un-abstracted it.

[fredrik-bakke]

Yeah, it's not very conceptual. The first half reasons using homotopies and the last half using identifications. There's another proof in HoTT-UF, but I decided to just brute force it.

[EgbertRijke]

Yeah, it's not very conceptual. The first half reasons using homotopies and the last half using identifications. There's another proof in HoTT-UF, but I decided to just brute force it.

I'll clean it up for you

[fredrik-bakke]

Yeah, it's not very conceptual. The first half reasons using homotopies and the last half using identifications. There's another proof in HoTT-UF, but I decided to just brute force it.

I'll clean it up for you

Under usual conditions, I would be more than happy to clean up my own mess as well given the feedback, although I also appreciate what you're doing!

[fredrik-bakke]

Is this PR closing completion? I was hoping to do a few more things with retracts of maps.

[EgbertRijke]

I'll try to complete it asap. But things are not done in sufficiently functorial manner, so I'm adding for example morphisms of arrows to make this possible.

[fredrik-bakke]

As agreed with Egbert, I will review and then merge this PR now. So if anyone else wants to give more input, now is your chance.

[fredrik-bakke]

Awesome work, Egbert! Thanks for doing all this

[fredrik-bakke]

I don't know if you intended to, but I noticed you didn't include the explanation of the terminology "6-for-2" as you did for "3-for-2".