Homotopy Type Theory dense strict order > history (Rev #1)

Definition

A strict order $\lt$ on a type $A$ is dense if for terms $a:A$ and $b:A$ , the open interval $(a, b)$ is inhabited

a:A, b:A \vdash \pi(a, b):\vert(a, b)\vert