I agree that the law of the excluded middle is true, but it is actually useful in a number of contexts to have equality types, and witnesses for two given terms

I agree that the law of the excluded middle is true, but it is actually useful in a number of contexts to have equality types, and witnesses for two given terms being equal. Of course, in some contexts when one has those types, it may be better to forget any distinction between different ways a witness to an equality can be produced, leaving identity types with at most one element. Just because the LEM is true doesn’t mean intuitionistic reasoning that avoids the use of the LEM isn’t sometimes useful.