## 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 ## * [[strict order]] * [[Dedekind cut]] * [[dense relation]] * [[locale of open intervals]]