UniMath
section?
Do you want to use the word "section" for an f : \prod_{x:A} B(x) ? We also have "family of elements" f(x) : B(x), for all x:A. If yes, we should add this terminology in 2.4.
Marc
I think I have managed to not use "section". Don't feel strongly about this, but the term MAY be alienating so I have instinctively avoided it.
I also avoided it, but Dan has used it. Dan, would you mind if I substitute all occurrences of section (that at neither Section nor \section) by function?
To me that'd suggest independent pi. I don't use a special word for it (as for elements in so many other types), But again I don't have a strong opinion
Bjorn
On 27 Mar 2019, at 20:15, Marc Bezem [email protected] wrote:
I also avoided it, but Dan has used it. Dan, would you mind if I substitute all occurrences of section (that at neither Section nor \section) by function?
— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.
Earlier I have used "dependent function", but that became cumbersome, so I dropped the "dependent" (after some discussion). We agreed once on allowing "map" for "function". If we also allow "section", we are quickly using up our credit of available terms. We would, for example, not be able to use the term "section" to single out the special case of a right inverse of a retraction.
I've searched for that and removed some places in the semidirect product section where I used "section".
Perhaps this usage may remain:
I also see this usage of Ulrik's ( @UlrikBuchholtz ) :
@DanGrayson I think yours is the use of section as a right-inverse.
@UlrikBuchholtz yours looks different to me, but we can of course have local special-purpose terminology when introduced explicitly.