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 classica

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.