## 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)$$ ## See also ## * [[strict order]] * [[closed interval]] * [[lower bounded open interval]] * [[upper bounded open interval]]