# Homotopy Type Theory algebraic limit field > history (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

# Contents

## Idea

A field with a notion of a limit of a function that satisfy the algebraic limit theorems.

## Definition

Let $F$ be a Heyting field and a function limit space, where $x^{-1}$ is another notation for $\frac{1}{x}$. $F$ is a algebraic limit field if the algebraic limit theorems are satisfied, i.e. if the limit preserves the ring operations:

$z:\prod_{c:S} \left(\lim_{x \to c} 0(x) = 0\right)$
$a:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) + g(x) = \lim_{x \to c} f(x) + \lim_{x \to c} g(x)\right)$
$n:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} -f(x) = -\lim_{x \to c} f(x) \right)$
$s:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) - g(x) = \lim_{x \to c} f(x) - \lim_{x \to c} g(x)\right)$
$\alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{a:\mathbb{Z}} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right)$
$\alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{a:S} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right)$
$o:\prod_{c:S} \left(\lim_{x \to c} 1(x) = 1\right)$
$m:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) \cdot g(x) = \lim_{x \to c} f(x) \cdot \lim_{x \to c} g(x)\right)$
$p:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{n:\mathbb{N}} \left(\lim_{x \to c} {f(x)}^n = {\left(\lim_{x \to c} f(x)\right)}^n \right)$

and the field operations:

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