Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In Archimedean ordered fields
Let be an Archimedean ordered field. The limit of a function approaching a term is a term such that for all directed types and nets where is the limit of , is the limit of , or written in type theory:
where
The limit is usually written as
In preconvergence spaces
Let and be preconvergence spaces. The limit of a function approaching a term is a term such that for all directed types and nets where is a limit of , is a limit of , or written in type theory:
In function limit spaces
Let be a function limit space and let be a subtype of . The limit of a function approaching is a term such that the limit of approaching is equal to :
We define the type of functions with limits approaching as the dependent type