Comment by aureianimus

With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.