## 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$$ ## See also ## * [[Heyting field]] * [[rational function]]