# Homotopy Type Theory reciprocal function > history (Rev #2, changes)

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

## Definition

Given a

Heyting field $F$, let us define the type of all terms in $F$ apart from 0:

$F_{#0} \coloneqq \left(\sum_{a:F} a # 0\right)$

The reciprocal function is a partial function

$f:F_{#0} \to F$

with terms

$\lambda:\prod_{a:F_{#0}} a \cdot f(a) = 1$
$\rho:\prod_{a:F_{#0}} f(a) \cdot a = 1$