# Homotopy Type Theory apartness relation > history (Rev #2)

## 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)$