# Homotopy Type Theory upper bounded open interval > history (Rev #1)

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