I wouldn't really say that it has a different type theory, just that it has proof irrelevance and functional extensionality build into the kernel as axioms. But

I wouldn't really say that it has a different type theory, just that it has proof irrelevance and functional extensionality build into the kernel as axioms. But yeah, it's a good way to show that you definitely don't have to give up LEM.