isomorphism of categories in mathlib?

Stream: mathlib4

[Emily Riehl]

This thread records a suggestion made by @Joël Riou on PR #25780 that is no longer relevant to that PR but should be recorded somewhere.

@Joël Riou notes:

In mathlib, we only have the notion of equivalence of categories, but no isomorphism of categories. This work suggests that even if we have kind of avoided introducing this notion until now, it would be a good idea to have a Prop typeclass Equivalence.IsIso, and a Equivalence.toEquiv which would allow to obtain bijections between types. By adding a few typeclasses about pre/post-composition with isomorphisms of categories, this should ease certain definitions in this PR.

The specific definitions are no longer included in that PR, so I'm not planning to act on this now. But I thought I'd check whether others agree that this would be useful API to have in Mathlib. If so, does someone want to implement it?