Homotopy Type Theory
irrational numbers > history (Rev #1)
Definition
Let be an Archimedean ordered integral domain with the integers being a integral subdomain of , with monic function . The apartness relation in and is defined as
and the non-zero integers are defined as
with monic function .
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 06:39:47 by
Anonymous?.
See the history of this page for a list of all contributions to it.