Homotopy Type Theory
irrational numbers > history (Rev #4, changes)
Showing changes from revision #3 to #4:
Added | Removed | Changed
Contents
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 . An The elementtight apartness relation is irrational if in is defined as
The An type element ofirrational numbers in is irrational if is defined as
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 April 17, 2022 at 23:00:26 by
Anonymous?.
See the history of this page for a list of all contributions to it.