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

Showing changes from revision #1 to #2: Added | Removed | Changed

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