search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Section-retraction pairs #119

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

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 commented 1 year ago

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

fredrik-bakke commented 1 year ago

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 commented 1 year ago

@TashiWalde

emilyriehl commented 1 year ago

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

fredrik-bakke commented 1 year ago

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 commented 1 year ago

"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 commented 1 year ago

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