Homotopy Type Theory dense strict order > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

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

See also

• strict order

• extended Dedekind cut

• dense relation

• locator

• locale of open intervals