## Definition ## Given a [[strictly ordered type]] $A$ and terms $a:A$ and $b:A$ an __open interval__ $(a, b)$ is a dependent type defined as $$(a, b) \coloneqq \sum_{c:A} (a \lt c) \times (c \lt b)$$ ## See also ## * [[strict order]] * [[closed interval]]