# Homotopy Type Theory decidable open interval > history (changes)

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

## Definition

Given a

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

$(a, b) \coloneqq \sum_{c:A} ((a \lt c) \wedge (c \lt b) = 1)$