Homotopy Type Theory open interval > history (changes)

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


< open interval

Given a

strictly ordered type AA and terms a:Aa:A and b:Ab:A, an element c:Ac:A is strictly between aa and bb if a<ca \lt c and c<bc \lt b

isStrictlyBetween(c,a,b)(a<c)×(c<b)isStrictlyBetween(c, a, b) \coloneqq (a \lt c) \times (c \lt b)

and an open interval (a,b)(a, b) is a dependent type defined as

(a,b) c:AisStrictlyBetween(c,a,b)(a, b) \coloneqq \sum_{c:A} isStrictlyBetween(c, a, b)

See also

Last revised on June 14, 2022 at 16:28:44. See the history of this page for a list of all contributions to it.