# Homotopy Type Theory limit of a binary function approaching a diagonal > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

# Contents

## Definition

Let $T$ be a function limit space with a tight apartness relation $\#$ and let $S \subseteq T$ be a subtype of $T$. Let us define the subtype $\Delta_{\#}(S) \subseteq S \times S$ of pairs of elements apart from the diagonal as

$\Delta_{\#}(S) \coloneqq \sum_{(x,y):S \times S} x \# y$

Let $U$ be a type such that $\Delta_{\#}(S) \subseteq U$ and $U \subseteq S \times S$. As a result, for every $x:S$, there is a dependent type

$U(x) \coloneqq \sum_{y:S} (x, y)$

Given a partial binary function $q:U \to T$, the currying of $q$ results in the dependent functions

$x:S \vdash q(x): \left(\sum_{y:U(x)} (x,y)\right) \to T$

A function $g:S \to T$ is a limit of $q$ approaching the diagonal if for all $x:S$ the limit of the dependent function $q(x)$ approaching $x$ is $g(x)$. We can define a predicate that the $q$ has a limit approaching the diagonal as

$hasLimitApproachingDiagonal(q) \coloneqq \left[\sum_{g:S \to T} \prod_{x:S} \lim_{y \to x} q(x)(y) = g(x)\right]$

The type of all functions in $U \to T$ that have a limit approaching the diagonal is defined as

$DiagLimFunc(S, T) \coloneqq \sum_{q:U \to T} hasLimitApproachingDiagonal(q)$

As a result, there exists a function

$\lim_{(x, y) \to (x, x)} (-)(x, y): DiagLimFunc(S, T) \to (S \to F)$

which returns the limit of a partial binary function $q:DiagLimFunc(S, T)$ approaching the diagonal and thus satisfies the equation

$\prod_{x:S} \lim_{y \to x} q(x)(y) = \lim_{(x, y) \to (x, x)} q(x, y)$

## Properties

In an algebraic limit field $F$, the algebraic limit theorems are satisfied:

### Limits preserve the zero function

$\prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = \lim_{y \to x} 0(x)(y)$
$\prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = 0$
$\prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = 0(x, x)$

### Limits preserve addition of functions

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{(x, y) \to (x, x)} (f + g)(x, y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} (f + g)(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} f(x)(y) + g(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} f(x)(y) + \lim_{y \to x} g(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) + \lim_{(x, y) \to (x, x)} g(x, y)$

### Limits preserve negation of functions

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = \lim_{y \to x} -f(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = -\lim_{y \to x} f(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = -\lim_{(x, y) \to (x, x)} f(x, y)$

### Limits preserve subtraction of functions

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{(x, y) \to (x, x)} (f - g)(x, y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} (f - g)(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} f(x)(y) - g(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} f(x)(y) - \lim_{y \to x} g(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) - \lim_{(x, y) \to (x, x)} g(x, y)$

### Limits preserve the left multiplicative $\mathbb{Z}$-action of functions

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{(x, y) \to (x, x)} (n f)(x, y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{y \to x} (n f)(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{y \to x} n f(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = n \lim_{y \to x} f(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = n \lim_{(x, y) \to (x, x)} f(x, y)$

### Limits preserve multiplication of functions by scalars

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{(x, y) \to (x, x)} (a f)(x, y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{y \to x} (a f)(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:f} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{y \to x} a f(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = a \lim_{y \to x} f(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = a \lim_{(x, y) \to (x, x)} f(x, y)$

### Limits preserve the one function

$\prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = \lim_{y \to x} 1(x)(y)$
$\prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = 1$
$\prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = 1(x, x)$

### Limits preserve multiplication of functions

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{(x, y) \to (x, x)} (f \cdot g)(x, y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} (f \cdot g)(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} f(x)(y) \cdot g(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} f(x)(y) \cdot \lim_{y \to x} g(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) \cdot \lim_{(x, y) \to (x, x)} g(x, y)$

### Limits preserve powers of functions

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{(x, y) \to (x, x)} (f^n)(x, y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{y \to x} (f^n)(x)(y)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{y \to x} (f(x)(y))^n$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \left(\lim_{y \to x} f(x)(y)\right)^n$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \left(\lim_{(x, y) \to (x, x)} f(x, y)\right)^n$

### Limits preserve reciprocals of functions

Where $x^{-1}$ is another notation for $\frac{1}{x}$

$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{(x, y) \to (x, x)} (f^{-1})(x, y)\right)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{y \to x} (f^{-1})(x)(y)\right)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{y \to x} (f(x)(y))^{-1}\right)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \left(\lim_{y \to x} f(x)(y)\right)^{-1}\right)$
$\prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \left(\lim_{(x, y) \to (x, x)} f(x, y)\right)^{-1}\right)$

### Limits preserve that the reciprocals of functions are multiplicative inverses

Where $x^{-1}$ is another notation for $\frac{1}{x}$

$\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{(x, y) \to (x, x)} (f \cdot f^{-1})(x, y)\right)$
$\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{y \to x} (f \cdot f^{-1})(x)(y)\right)$
$\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{y \to x} f(x)(y) \cdot {f(x)(y)}^{-1}\right)$
$\prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = 1\right)$