#Contents# * table of contents {:toc} ## Idea ## A general structure where the concept of [[limit of a function]] makes sense. ## Definition ## A __function limit space__ is a type $T$ such that for all [[subtype]]s $S \subseteq T$, there is a [[partial function]] $$\lim_{x \to (-)} (-)(x): S \times (S \to T) \to_\mathcal{U} T$$ called the __limit of $f:S \to T$ approaching $c:S$__. ## See also ## * [[limit of a function]] * [[pointwise continuous function]]