Homotopy Type Theory function limit space > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed


< function limit space


A general structure where the concept of limit of a function makes sense.


A function limit space is a type TT such that for all subtypes STS \subseteq T, there is a partial function

lim x()()(x):S×(ST) 𝒰T\lim_{x \to (-)} (-)(x): S \times (S \to T) \to_\mathcal{U} T

called the limit of f:STf:S \to T approaching c:Sc:S.

See also

Revision on June 10, 2022 at 13:33:07 by Anonymous?. See the history of this page for a list of all contributions to it.