Homotopy Type Theory
irrational numbers > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
Contents
< irrational numbers
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
Let be an Archimedean ordered integral domain with the integers being a integral subdomain of , with injection . The tight apartness relation in is defined as
An element is irrational if
The set of irrational numbers in is defined as
In homotopy type theory
Let be an Archimedean ordered integral domain with the integers being a integral subdomain of , with monic function . The tight apartness relation in is defined as
Let us define the dependent type on
is irrational if the type has a term.
The type of irrational numbers in is defined as:
See also
Revision on June 15, 2022 at 18:46:35 by
Anonymous?.
See the history of this page for a list of all contributions to it.