Section-retraction pairs

[TashiWalde]

As promised to @fredrik-bakke , some more expository material on section retraction pairs.
I also moved the definition of is-retract-of from 06-contractible to 03-equivalences to have it all in one place.

[fredrik-bakke]

Very good :)

[fredrik-bakke]

If you are done with this PR, I think you can go ahead and merge it

[fredrik-bakke]

Reading through parts of the repository now, I wonder if a better name for your section-retraction pairs is "mutual section-retraction pairs". What do you think about that name? This way, there can be no confusion about their relation.

[fredrik-bakke]

@TashiWalde

[emilyriehl]

@fredrik-bakke I'm a little behind. Could you give an example where you think this name is a good fit?

[fredrik-bakke]

Hi, @emilyriehl. Tashi provided the following relevant explanation for section-retraction pairs:

A consequence of the above is that in a section-retraction pair (s, r), the
map s is a section and the map r is a retraction. Note that not every
composable pair (s, r) of such maps is a section-retraction pair; they have to
(up to composition with an equivalence) be section and retraction of each
other.

It seems to me that it would not be unreasonable to conflate "section-retraction pair" with a composable pair of section and retraction. By using "mutual section-retraction pair", it is immediately clear that the section and retraction have a special relation to one another, and what that relation is would not be hard to intuit from the added adjective.

[TashiWalde]

"Section-retraction pair" is the terminology I have mostly used and seen used, but I don't mind if you want to change it to "mutual section-retraction pair". I don't really have a strong preference either way.

[fredrik-bakke]

I don't know, I just wanted to run my idea by you. If this is established terminology then I say we keep it.