Homotopy Type Theory decidable open interval > history (changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

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

Definition

< open interval

Given a

category: redirected to nlab
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?

category: not redirected to nlab yet

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

EditDiscussPrevious revisionHide changesHistory (2 revisions) Print Source