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

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