Very true. But the most popular ones are based on DTT, GP only mentioned Lean/Coq/Idris.

Indeed by sacrificing the power of type system we can augment classical axioms consistently as shown by HOL family.

These come with their own disadvantages.