Homotopy Type Theory decidable open interval > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed


< open interval

Given a

decidable strictly ordered set AA and terms a:Aa:A and b:Ab:A, an element c:Ac:A is strictly between aa and bb if (a<c)=1(a \lt c) = 1 and (c<b)=1(c \lt b) = 1 and a decidable open interval (a,b)(a, b) is a dependent type defined as

(a,b) c:A((a<c)(c<b)=1)(a, b) \coloneqq \sum_{c:A} ((a \lt c) \wedge (c \lt b) = 1)

See also

  • decidable strict order

  • decidable closed interval?

  • decidable lower bounded open interval?

  • decidable upper bounded open interval?

Last revised on June 18, 2022 at 21:55:27. See the history of this page for a list of all contributions to it.