Homotopy Type Theory open interval > history (Rev #3, changes)

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

Definition

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

Revision on April 21, 2022 at 21:40:34 by Anonymous?. See the history of this page for a list of all contributions to it.