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

Definition

Given a strictly ordered type $A$ and a term $a:A$ , a lower bounded open interval $(a, \infty)$ is a dependent type defined as

(a, \infty) \coloneqq \sum_{b:A} (a \lt b)