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

See also

• strict order

• open interval

• lower bounded open interval