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

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Definition

Given a strictly ordered type $A$ and terms $a:A$ and $b:A$ , an element~~open interval~~ $c:A$ is ~~$(a, b)$~~ strictly between is a ~~dependent~~ ~~type~~ ~~defined~~ as $a$ and $b$ if $a \lt c$ and $c \lt b$

isStrictlyBetween (c, a, b) ≔ \sum_{c : A} (a < c) \times (c < b)

~~(a,~~ isStrictlyBetween(c, a, b) \coloneqq ~~\sum_{c:A}~~ (a \lt c) \times (c \lt b)

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

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

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

Definition

See also