I am saying that Martin-Löf would see his work in Lean, not mathlib. Mathlib is a library. In Lean you can "contain" classic reasoning to certain parts of the code base, and that is also true in the original MLTT: you can postulate classical axioms as functions in scope.