Homotopy Type Theory
irrational numbers > history (Rev #2)
Definition
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 March 15, 2022 at 16:38:09 by
Anonymous?.
See the history of this page for a list of all contributions to it.