# Homotopy Type Theory rational function > history (Rev #1)

## Definition

Given a Heyting field $F$, let $f:F \to F$ and $g:F \to F$ be polynomial functions? and let $h:F_{#0} \to F$ be the reciprocal function of $F$. A rational function is a partial function

$k:\left(\sum{a:f} g(a) # 0\right) \to F$

defined as

$k(a) \coloneqq f(a) \cdot h(g(a))$