Commit 2025-02-19 20:44 f84c0cc9

feat(Order/Category): ConcreteCategory instance for CompleteLat (#21410) Upgrade CompleteLat to a concrete category.

I replace Bundled with a custom structure and make of an abbrev in order to make coe_of reducible.