Commit 2020-04-28 06:54 ae06db33

feat(category_theory/concrete): make constructing morphisms easier (#2502) Previously, if you wrote:

example (R : CommMon.{u}) : R ⟶ R :=
{ to_fun := λ x, _,
  map_one' := sorry,
  map_mul' := sorry, }

you were told the expected type was ↥(bundled.map comm_monoid.to_monoid R), which is not particularly reassuring unless you understand the details of how we've set up concrete categories. If you called dsimp, this got better, just giving R.α. This still isn't ideal, as we prefer to talk about the underlying type of a bundled object via the coercion, not the structure projection. After this PR, which provides a slightly different mechanism for constructing "induced" categories from bundled categories, the expected type is exactly what you might have hoped for: ↥R. There seems to be one place where we used to get away with writing 𝟙 _ and now have to write 𝟙 A, but otherwise there appear to be no ill-effects of this change. (For follow-up, I think I can entirely get rid of our local attribute [reducible] work-arounds when setting up concrete categories, and in fact construct most of the instances in @[derive] handlers, but these will be separate PRs.)