Comment by semolinapudding

Even without Mathlib, Lean's type theory is impredicative. Martin-Löf does not consider impredicativity to be constructive.