Homotopy Type Theory
interval-complete strict order > history (Rev #3)
Idea
Dedekind completeness but without the located requirement.
Defintion
A type with a strict order is interval-complete if
- For all terms and , the open interval is inhabited.
- For all terms and , if and only if is a subinterval of
(for all propositions and , )
- For all terms and , if and only if is a subinterval of
- For all terms and , the intersection of and is a subinterval of the open interval
See also
Revision on May 12, 2022 at 00:47:03 by
Anonymous?.
See the history of this page for a list of all contributions to it.