[[!redirects apartness space]] [[!redirects inequality space]] [[!redirects tight apartness relation]] ## Definition ## An __apartness relation__ on a type $A$ is a dependent type $a # b$ with dependent terms $$i(a): (a # a) \to \emptyset$$ $$s(a, b): (a # b) \to (b # a)$$ $$c(a, b, c): (a # b) \to \Vert (a # c) + (c # b) \Vert$$ $A$ is called an __apartness space__ or __inequality space__ An apartness relation is a __tight apartness relation__ if it additionally comes with dependent terms $$e(a, b): ((a # b) \to \emptyset) \to (a = b)$$ ## See also ## * [[binary relation]] * [[strict order]] * [[setoid]]