Finally, let us also say something about disequality, which is negation of equality:11We use “inequality” to refer to and . Also, note that this is negation of the propositional identity type. Of course, it makes no sense to negate judgmental equality , because judgments are not subject to logical operations.
If , we say that and are unequal or not equal. Just like negation, disequality plays a less important role here than it does in classical mathematics. For example, we cannot prove that two things are equal by proving that they are not unequal: that would be an application of the classical law of double negation, see §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic).
Sometimes it is useful to phrase disequality in a positive way. For example, in Theorem 11.2.4 (http://planetmath.org/1122dedekindrealsarecauchycomplete#Thmprethm1) we shall prove that a real number has an inverse if, and only if, its distance from is positive, which is a stronger requirement than .