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

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

# Contents

## 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 subtypes $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$.