#
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$

## See also

Revision on March 11, 2022 at 16:51:30 by
Anonymous?.
See the history of this page for a list of all contributions to it.