Commit 2024-12-14 12:11 b09464fc
View on Github →style(Algebra/Category/Grp/Basic and Algebra/Category/MonCat/Basic): universe order in uliftFunctor (#19957)
Change the order of universes in the uliftFunctors on the group and monoid categories so they will agree with the order used for CategoryTheory.uliftFunctor and SSet.uliftFunctor (that is, uliftFunctor.{u,v} should go from the category of doodads in Type v to the category of similar doodads in Type (max v u)).