Bezem and Coquand recently gave a constructive proof of decidability for the equational theory of arbitrary semi-lattices with an inflationary morphism, whose complexity is (weakly) polynomial. In this talk, we will present a mechanically verified (in Rocq) refinement of this algorithm, and a new design and implementation of cumulative universe polymorphism for dependent type theories, materialized in a branch of the Rocq prover. Our system handles universe level polymorphism for the full algebra (0, +1, max), using polynomial time constraint satisfiability and validity checking algorithms. We also generalize the notion of variance for universes to cumulative definitions, and design a new simplification algorithm allowing to infer minimal abstractions of universes and constraints for implicitly universe polymorphic definitions and proofs, while maintaining generality. We will present all these aspects along with examples, preliminary performance benchmarks and compatibility status.