Homotopy Type Theory decidable open interval > history (Rev #2)


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?

Revision on June 15, 2022 at 22:47:42 by Anonymous?. See the history of this page for a list of all contributions to it.