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