mathlib

313cc2fe - chore(category_theory/concrete_category): take an instance, rather than extending, category (#2195)

chore(category_theory/concrete_category): take an instance, rather than extending, category (#2195) chore(category_theory/concrete_category): take an instance, rather than extending, category (#2195) Our current design for `concrete_category` has it extend `category`. This PR changes that so that is takes an instance, instead. I want to do this because I ran into a problem defining `concrete_monoidal_category`, which is meant to be a monoidal category, whose faithful functor to Type is lax monoidal. (The prime example here is `Module R`, where there's a map `F(X) \otimes F(Y) \to F(X \otimes Y)`, but not the other way: here `F(X) \otimes F(Y)` is just the monoidal product in Type, i.e. cartesian product, and the function here is `(x, y) \mapsto x \otimes y`.) Now, `monoidal_category` does not extend `category`, but instead takes a typeclass, so with the old design `concrete_monoidal_category` was going to be a Frankenstein, extending `concrete_category` and taking a `[monoidal_category]` type class. However, when 3.7 landed this went horribly wrong, and even defining `concrete_monoidal_category` caused an unbounded typeclass search. So.... I've made everything simpler, and just not used `extends` at all. It's all just typeclasses. This makes some places a bit more verbose, as we have to summon lots of separate typeclasses, but besides that everything works smoothly. (Note, this PR makes the change to `concrete_category`, but does not yet introduce `concrete_monoidal_category`.)