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

## 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):\left[(a, b)\right]$

## See also

Revision on June 10, 2022 at 15:50:15 by
Anonymous?.
See the history of this page for a list of all contributions to it.