Homotopy Type Theory
irrational numbers > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Definition
Let be an Archimedean ordered integral domain with the integers being a integral subdomain of , with monic function . The tight apartness relation in and is defined as
and Let us define the non-zero dependent integers type are on defined as
with monic function is irrational if the type . has a term.
Let The us define the dependent type on ofirrational numbers in is defined as:
is irrational if the type has a term.
The type of irrational numbers in is defined as:
See also
Revision on March 15, 2022 at 16:38:09 by
Anonymous?.
See the history of this page for a list of all contributions to it.