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

Showing changes from revision #0 to #1: Added | ~~Removed~~ | ~~Chan~~ged

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