mathlib

2634c1b5 - feat(category_theory/cones): map_cone_inv as an equivalence (#4253)

feat(category_theory/cones): map_cone_inv as an equivalence (#4253) When `G` is an equivalence, we have `G.map_cone_inv : cone (F ⋙ G) → cone F`, and that this is an inverse to `G.map_cone`, but not quite that these constitute an equivalence of categories. This PR fixes that. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>