## Definition ## Given a [[strictly ordered type]] $A$ and a term $a:A$, an __upper bounded open interval__ $(a, \infty)$ is a dependent type defined as $$(-\infty, a) \coloneqq \sum_{b:A} (b \lt a)$$ ## See also ## * [[strict order]] * [[open interval]] * [[lower bounded open interval]]