Mate equivalence for "transformations of equivalences"

Stream: Is there code for X?

[Robin Carlier]

docs#CategoryTheory.conjugateEquiv has the following TODO:

TODO: Generalise to when the two vertical functors are equivalences rather than being exactly `𝟭`.

Am I right to assume this has not been cleared yet? I need it and want to ask for confirmation before working on it. @Joël Riou do you maybe know (or, even better, already have code in that direction)?

[Joël Riou]

I have not worked on this.