Commit 2026-04-26 07:51 af51d9db

chore(CategoryTheory): deprecate ConcreteCategory.instFunLike (#38443) This non-instance instance was a remainder from the old ConcreteCategory API, which was then renamed to HasForget and was parallel to the current ConcreteCategory API for some time, but has now been completely removed. This instance should never be used, ConcreteCategory comes with a FunLike instance on the FC parameter, which is what should be used instead.