nLab inequality space


(0,1)(0,1)-Category theory




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Constructivism, Realizability, Computability



A strict inequality relation or tight apartness relation #\# is an apartness relation which is also a tight relation. An inequality space is a set with a strict inequality relation. Strict inequalities are contrasted with weak inequality or denial inequality, which is the negation of equality. In the context of excluded middle, every weak inequality is a strict inequality relation, so one simply talks about “inequality”.


In set theory

In set theory, an inequality space is a set SS with a binary relation #\# such that

  • for all aSa \in S, ¬(a#a)\neg(a \# a)
  • for all aSa \in S and bSb \in S, a#ba \# b implies b#ab \# a
  • for all aSa \in S, bSb \in S, and cSc \in S, a#ca \# c implies that either a#ba \# b or b#cb \# c
  • for all aSa \in S and bSb \in S, a=ba = b if and only if ¬(a#b)\neg(a \# b)

In dependent type theory

In dependent type theory, an inequality space is a type TT with

  • a type family a:T,b:Ta#btypea:T, b:T \vdash a \# b \; \mathrm{type}
  • a family of terms a:T,b:Tproptrunc(a,b):isProp(a#b)a:T, b:T \vdash \mathrm{proptrunc}(a, b):\mathrm{isProp}(a \# b)
  • a family of terms a:Tirr(a):(a#a)𝟘a:T \vdash \mathrm{irr}(a):(a \# a) \to \mathbb{0}
  • a family of terms a:T,b:Tsym(a,b):(a#b)(b#a)a:T, b:T \vdash \mathrm{sym}(a, b):(a \# b) \to (b \# a)
  • a family of terms a:T,b:T,c:Tcom(a,b,c):(a#c)[(a#b)+(b#c)]a:T, b:T, c:T \vdash \mathrm{com}(a, b, c):(a \# c) \to \left[(a \# b) + (b \# c)\right]
  • a family of terms a:T,b:Ttight(a,b):isEquiv(idtonotapart(a,b))a:T, b:T \vdash \mathrm{tight}(a, b):\mathrm{isEquiv}(\mathrm{idtonotapart}(a, b))

where a:T,b:Tidtonotapart(a,b):(a= Tb)((a#b)𝟘)a:T, b:T \vdash \mathrm{idtonotapart}(a, b):(a =_T b) \to ((a \# b) \to \mathbb{0}) is inductively defined by

a:Tβ idtonotapart refl T(a):idtonotapart(a,a)(refl T(a))= (a#a)𝟘irr(a)a:T \vdash \beta_{\mathrm{idtonotapart}}^{\mathrm{refl}_T}(a):\mathrm{idtonotapart}(a, a)(\mathrm{refl}_T(a)) =_{(a \# a) \to \mathbb{0}} \mathrm{irr}(a)

The last condition ensures that the type is an h-set.


Strongly extensional functions

Given two inequality spaces SS and TT, a function f:STf\colon S \to T is strongly extensional if f(x)#f(y)f(x) \# f(y) implies x#yx \# y; that is, ff reflects apartness. ff is a strongly injective if f(x)#f(y)f(x) \# f(y) is logically equivalent to x#yx \# y. The contrapositive of the both conditions imply that ff preserves equality and is an injection respectively.

Stable and decidable inequality

Strict inequality is stable if it is logical equivalent to denial inequality; i.e. for all elements aSa \in S and bSb \in S, aba \neq b if and only if a#ba \# b. Stable strict inequality is simply called “inequality”, as there is no need to distinguish between strict inequality and denial inequality in this case.

Strict inequality is decidable if for all elements aSa \in S and bSb \in S, a#ba \# b or a=ba = b. Decidable strict inequality implies stable strict inequality, so it is usually called decidable inequality. In the context of excluded middle, every strict inequality relation is decidable.

The category of inequality spaces

In the category of inequality spaces, monomorphisms between inequality spaces are strongly extensional functions that preserve strict inequality, or strong injections. These monomorphisms are regular monomorphisms. The category of inequality spaces has all (small) limits, created by the forgetful functor to Set. (For example, (a,b)#(x,y)(a,b) \# (x,y) iff a#xa \# x or b#yb \# y.) Similarly, it has all finite coproducts, and it has quotients of equivalence relations. In fact, this category is a complete pretopos. It is not, however, a Grothendieck topos (or even a topos at all), because it doesn't have all infinite coproducts. (To be precise, the statement that it has all small coproducts, or even that it has a subobject classifier, seems to be equivalent to excluded middle.)

We can say, however, that it has coproducts indexed by inequality spaces, although to make this precise is a triviality. More interestingly, it has products indexed by inequality spaces; that is, it is (even locally) a cartesian closed category. In particular, given inequality spaces XX and YY, the set StrExt(X,Y)\StrExt(X,Y) of strongly extensional functions from XX to YY becomes an inequality space under the rule that f#gf \# g iff f(x)#g(x)f(x) \# g(x) for some x:Xx\colon X.

Foundational status

In set theory

In classical mathematics, it is true that every set is an inequality space. In constructive mathematics, however, not all sets are inequality spaces. Instead, one can add an axiom to the foundations of mathematics which states that every set is an inequality space.

Axiom of inequality spaces: Every set has a strict inequality relation.

Alternatively, one could take the strict inequality to be foundational, in which the axiom of extensionality becomes

Axiom of extensionality: for any set xx and yy, ¬(x#y)\neg(x \# y) if and only if for all zz, zxz \in x if and only if zyz \in y.

In dependent type theory

In dependent type theory, one can make every type into an inequality space by adding the following set of rules to the type theory:

ΓAtypeΓ,a:A,b:Aa#btypeΓAtypeΓ,a:A,b:Aproptrunc(a,b):isProp(a#b)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash a \# b \; \mathrm{type}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{proptrunc}(a, b):\mathrm{isProp}(a \# b)}
ΓAtypeΓ,a:Airr(a):(a#a)𝟘ΓAtypeΓ,a:A,b:Asym(a,b):(a#b)(b#a)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{irr}(a):(a \# a) \to \mathbb{0}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{sym}(a, b):(a \# b) \to (b \# a)}
ΓAtypeΓ,a:A,b:A,c:Acomp(a,b,c):(a#c)[(a#b)+(b#c)]\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A, c:A \vdash \mathrm{comp}(a, b, c):(a \# c) \to \left[(a \# b) + (b \# c)\right]}
ΓAtypeΓ,a:A,b:Aidtonotapart(a,b):(a= Ab)((a#b)𝟘)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{idtonotapart}(a, b):(a =_A b) \to ((a \# b) \to \mathbb{0})}
ΓAtypeΓ,a:Aidtonotapart(a,a)(refl A(a))irr(a):(a#a)𝟘\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{idtonotapart}(a, a)(\mathrm{refl}_A(a)) \equiv \mathrm{irr}(a):(a \# a) \to \mathbb{0}}
ΓAtypeΓ,a:A,b:Atight(a,b):isEquiv(idtonotapart(a,b))\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash \mathrm{tight}(a, b):\mathrm{isEquiv}(\mathrm{idtonotapart}(a, b))}

This implies axiom K and uniqueness of identity proofs.

In algebra

Since inequality spaces have finite limits, the usual constructions of universal algebra apply; it's straightforward to define inequality groups, inequality rings, and so on.

The various subsets that appear in algebra (such as subgroups, ideals, and cosets) become less fundamental than certain subsets that are, classically, simply their complements. For example, a left ideal in a ring RR is a subset II such that 0I0 \in I, x+yIx + y \in I whenever x,yIx, y \in I, and xyIx y \in I whenever xIx \in I. But a left antiideal in an inequality ring RR is an #\#-open subset AA such that 0A0 \in A is false, xAx \in A or yAy \in A whenever x+yAx + y \in A, and xAx \in A whenever xyAx y \in A. (The #\#-openness requirement is automatic if ¬(0A)\neg(0\in A) is strengthened to p#0p\# 0 for all pAp\in A, using that the ring operations are strongly extensional.) Note that the complement of an antiideal is an ideal, but not every ideal can be constructively shown to be the complement of an antiideal; so antiideals are more fundamental than ideals, in an inequality ring.

Prime ideals are even more interesting. A two-sided antiideal AA (so also satisfying that yAy \in A whenever xyAx y \in A) is antiprime (or simply prime if no confusion is expected) if 1A1 \in A and xyAx y \in A whenever x,yAx, y \in A. Now the complement of an antiprime antiideal may not be a prime ideal (as normally defined). But in fact, it is antiprime antiideals that are more important in constructive algebra. In particular, an integral domain in constructive algebra is an inequality ring in which the antiideal of nonzero elements is antiprime.

Any apartness relation on an inequality space XX is the same as the (strongly) closed equivalence relation on the discrete locale XX. This localic perspective on apartness relations extends naturally to anti-algebra: an antiideal is the same as a closed ideal in a discrete localic ring that respects the closed equivalence relation corresponding to #\#. Equivalently, this is a closed ideal of the #\#-topology regarded as a (non-discrete) localic ring. The spatial part of this closed localic ideal is then the ordinary ideal complementary to the antiideal, and so on. Moreover, since unions of closed sublocales correspond to intersections of their open complements, an antiideal AA is antiprime exactly when its corresponding closed localic ideal CA\mathsf{C}A is “prime” in an appropriate internal sense in Loc, namely that m *(CA)(CA×R)(R×CA)m^*(\mathsf{C}A) \subseteq (\mathsf{C}A \times R) \cup (R\times \mathsf{C}A), where m:R×RRm:R\times R\to R is the multiplication. The fact that the complement of an antiprime antiideal need not be prime in the usual sense corresponds to the fact that taking the spatial part of sublocales doesn’t commute with unions.

For more about apartness algebra, see antisubalgebra.


  • Anne Troelstra's and Dirk van Dalen's Constructivism in Mathematics (1988) uses “preapartness” and “apartness” instead of “apartness” and “strict inequality”/“tight apartness” respectively.

Last revised on January 18, 2024 at 15:07:56. See the history of this page for a list of all contributions to it.