## 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)$$ ## See also ## * [[decidable strict order]] * [[decidable closed interval]] * [[decidable lower bounded open interval]] * [[decidable upper bounded open interval]] category: not redirected to nlab yet