Contemporary type theories have little issue with adding the law of excluded middle as an axiom, though for some intensional type theories it will end up being

Contemporary type theories have little issue with adding the law of excluded middle as an axiom, though for some intensional type theories it will end up being the only axiom that doesn’t reduce (i.e. have a computational rule associated during simplification) in a useful way. Programming language type systems rarely form consistent logics so there introducing it has no real effect either way.