#
Homotopy Type Theory
apartness relation > history (changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

~~
~~## 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

~~
~~
Last revised on June 15, 2022 at 20:55:51.
See the history of this page for a list of all contributions to it.