Let be the rational numbers and let be the type of positive rational numbers. Given a directed type , a term is a limit of a net or that converges to if comes with a term
The type of all limits of a net is defined as
A limit of a sequence is usually written as
In Archimedean ordered fields
Let be an Archimedean ordered field and let be the type of positive rational numbers. Given a directed type , a term is a limit of a net or that converges to if comes with a term
The type of all limits of a net is defined as
A limit of a sequence is usually written as
Most general definition
Let be a type with a predicate between the type of all nets in
and itself.
Given a directed type , a term is a limit of a net or that converges to if the proposition is contractible.