mathlib3

3edb6a4a - fix(category_theory/concrete): access the carrier type by the coercion (#2473)

fix(category_theory/concrete): access the carrier type by the coercion (#2473) This should marginally reduce the pain of using concrete categories, as the underlying types of a bundled object should more uniformly described via a coercion, rather than the `.α` projection. (There's still some separate pain involving `bundled.map`, but it has an orthogonal fix which I'm working on in another branch.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>