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

## See also

Revision on June 14, 2022 at 20:31:14 by
Anonymous?.
See the history of this page for a list of all contributions to it.