#
Homotopy Type Theory
open interval > history (changes)

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

## Definition

< open interval

~~Given a ~~

~~strictly ordered type~~~~ ~~~~$A$~~~~ and terms ~~~~$a:A$~~~~ and ~~~~$b:A$~~~~, an element ~~~~$c:A$~~~~ is ~~**strictly between**~~ ~~~~$a$~~~~ and ~~~~$b$~~~~ if ~~~~$a \lt c$~~~~ and ~~~~$c \lt b$~~~~
~~$isStrictlyBetween(c, a, b) \coloneqq (a \lt c) \times (c \lt b)$

~~
~~and an **open interval** $(a, b)$ is a dependent type defined as

~~
~~$(a, b) \coloneqq \sum_{c:A} isStrictlyBetween(c, a, b)$

~~
~~## See also

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