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

Definition

Given a strictly ordered type $A$ and terms $a:A$ and $b:A$ an open interval $(a, b)$ is a dependent type defined as

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