Notation for transitivity of equivalences of categories

Stream: mathlib4

[Robin Carlier]

Transitivity of isomorphisms in a category has the ≪≫ notation, which I find very nice as it reflects the idea that isomorphisms are "undirected". I realized that there is an abbreviation (\Ll) for the symbol ⋘ as well, and so it could be possible to introduce the notation ⋘⋙ for Equivalence.Trans, which would extends nicely the way the notation ⋙ for functor composition mimics the notation ≫ for morphism composition.

What are the CategoryTheorymaintainers thoughts on such a notation?

[Yaël Dillies]

How much use do you expect for this new symbol?

[Robin Carlier]

As much use as there are for commutavive diagrams of equivalences of categories :smiley:. Playing with equivalences, functors and so on gets very very verbose easily, and that could alleviate that a bit.
For instance, if you were to phrase the pentagon axiom for product of categories, you'd have to put .trans everywhere, which is cumbersome.
I also feel that such a notation reflects the philosophy that equivalences are undirected the same way isomorphisms are.