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

Definition

An apartness relation on a type AA is a dependent type a#ba # b with dependent terms

i(a):(a#a)i(a): (a # a) \to \emptyset
s(a,b):(a#b)(b#a)s(a, b): (a # b) \to (b # a)
c(a,b,c):(a#b)(a#c)+(c#b)c(a, b, c): (a # b) \to \Vert (a # c) + (c # b) \Vert

AA 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))(a=b)e(a, b): ((a # b) \to \emptyset) \to (a = b)

See also

Revision on March 15, 2022 at 00:20:45 by Anonymous?. See the history of this page for a list of all contributions to it.