UniMath
Path concatenation or composition, or both?
We are not consistently using "concatenation" of paths, but sometimes also "composition". What do we prefer? 2.3 defines "concatenation". Paths over are currently composed (my mistake).
We should be consistent, and "concatenation" seems to be the better choice, since "composition" is in use for functions, and since it conveys a geometric connotation.
I vote for both, maybe with a preference for “concatenation” when using diagrammatic order (﹡), and “composition” when using “classical” order (∘,·).
I always prefer composition, but look kindly on believers of other faiths as long as they leave me to die in my sinful ways (perhaps with the exception of those who write textbooks I have to teach from).
Bjorn
[I have a very simple mind, and was overjoyed the day someone taught me about the opposite category which allowed me to forget about which was which of contravariant and covariant - Spivak had a fun rant about just that, though - and left me with functors only. I have it the same way with functions, modules, G-sets etc, etc. ]
On Sat, May 23, 2020 at 5:26 PM Ulrik Buchholtz [email protected] wrote:
I vote for both, maybe with a preference for “concatenation” when using diagrammatic order (﹡), and “composition” when using “classical” order (∘,·).
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/UniMath/SymmetryBook/issues/72#issuecomment-633075958, or unsubscribe https://github.com/notifications/unsubscribe-auth/AKO2SK3VX6VJTNU5ENYQHMDRS7TLRANCNFSM4NIPQCHA .
The consensus seems to be to introduce both terms initially as synonyms, and to point out the "composition" is used also for functions. Mention the relationship via univalence or transport.
See what I did in 07ddd9e7632b43b68af98354cc26f8aded6ac1bf. I didn't mention univalence explicitly, since univalence comes much later, but I mentioned transport.