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)$