mathlib3

616cb5e6 - chore(category_theory/equivalence) explicit transitivity transformation (#3176)

chore(category_theory/equivalence) explicit transitivity transformation (#3176) Modifies the construction of the transitive equivalence to be explicit in what exactly the natural transformations are. The motivation for this is two-fold: firstly we get auto-generated projection lemmas for extracting the functor and inverse, and the natural transformations aren't obscured through `adjointify_η`.