¹¹We 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.