3 ms·
With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.
by aureianimus 10mo ago
With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.