Commit 2020-04-02 08:17 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) 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.)