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

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

## 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\u22a2\pi (a,b):\Vert [(a,b)](a,b)\Vert $$ a:A, b:A \vdash \pi(a,~~ b):\Vert(a,~~ b):\left[(a,~~ b)\Vert~~ b)\right]

## See also

Revision on April 21, 2022 at 13:23:13 by
Anonymous?.
See the history of this page for a list of all contributions to it.