Homotopy Type Theory
irrational numbers > history (Rev #4)
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 . 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 April 17, 2022 at 23:00:26 by
Anonymous?.
See the history of this page for a list of all contributions to it.