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

Showing changes from revision #3 to #4: 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

 a:A, b:A \vdash \pi(a, b):\Vert(a, b):\left[(a, b)\Vert b)\right]