Commit 2020-06-26 01:23 616cb5e6

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_η.