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

Showing changes from revision #7 to #8:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

< DLO

~~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

~~
~~
Last revised on June 14, 2022 at 16:27:16.
See the history of this page for a list of all contributions to it.