# Homotopy Type Theory open interval > history (changes)

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

## Definition

Given a

strictly ordered type $A$ and terms $a:A$ and $b:A$, an element $c:A$ is strictly between $a$ and $b$ if $a \lt c$ and $c \lt b$

$isStrictlyBetween(c, a, b) \coloneqq (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)$