Once you have an infinite hierarchy of types, including universe levels, can the proof assistant really be "as simple as possible"?
I feel like a simple-as-possible proof assistant would be more like, proving things about programs written in a minimal Lisp dialect, where the proof validator is itself written in that Lisp dialect.
That said, I personally would rather have an extremely usable proof assistant, rather than a simple-as-possible one. In many ways those things point in opposite directions; consider the usability and simplicity of Python vs the lambda calculus.
I feel like a simple-as-possible proof assistant would be more like, proving things about programs written in a minimal Lisp dialect, where the proof validator is itself written in that Lisp dialect.
That said, I personally would rather have an extremely usable proof assistant, rather than a simple-as-possible one. In many ways those things point in opposite directions; consider the usability and simplicity of Python vs the lambda calculus.