Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
basic constructions:
strong axioms
further
A weak inequality relation or denial inequality relation on a set is the negation of the equality relation on .
This is a term found in constructive mathematics, to distinguish from strict inequality relation or other notions of inequality relation such as tight apartness relations. In classical mathematics, weak inequality relations and strict inequality relations are the same and are simply called “inequality”, so the notion plays no further role classically.
If one wishes to reserve the word “inequality” for order relations (such as and ), then one may instead use the word disequality to refer to the weak inequality. (For instance, this is common in type theory with subtype relations that form an ordering on the types.)
The weak inequality relation is an irreflexive symmetric relation. Irreflexivity follows from the negation of reflexivity of equality, while symmetry follows from the contrapositive of symmetry of equality. In addition, the weak inequality relation is a stable relation, because in constructive mathematics, given any proposition , implies that . This means that implies that , and since if and only if , this means that implies that . Weak inequality is a weakly tight relation, in that for all elements and , implies that , because by definition, if and only if , and so by contraposition, if and only if .
The denial inequality relation on a set is said to be a denial apartness relation if for all elements , and , implies that .
This implies that is an apartness relation because the contrapositive of the transitive property of equality states that implies that , and the above condition implies that , which is precisely the condition for a comparison.
In particular, if de Morgan's law holds in the logic, then every weak inequality relation is a denial apartness relation.
Similarly, every stable tight apartness relation is a denial apartness relation.
Last revised on January 18, 2024 at 15:07:27. See the history of this page for a list of all contributions to it.