Commit 2025-01-17 15:43 9ca037a4

feat(CategoryTheory): define unbundled ConcreteCategory class (#20810) This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR defines a new class ConcreteCategory that unbundles the coercion of morphisms to functions and objects to types, in order to allow ConcreteCategory to coexist alongisde existing coercions to functions/sorts. No instances are included yet, since those can be declared in parallel. See e.g. CommRingCat on the redesign-ConcreteCategory branch for examples of what a concrete category instance will end up looking like.