Homotopy Type Theory
interval-complete strict order > history (Rev #4, changes)
Showing changes from revision #3 to #4:
Added | Removed | Changed
Idea
< Dedekind completion
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 June 10, 2022 at 14:50:21 by
Anonymous?.
See the history of this page for a list of all contributions to it.