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

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

Definition

< reciprocal function

Given a

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

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

The reciprocal function is a partial function

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

with terms

λ: a:F #0af(a)=1\lambda:\prod_{a:F_{#0}} a \cdot f(a) = 1
ρ: a:F #0f(a)a=1\rho:\prod_{a:F_{#0}} f(a) \cdot a = 1

See also

Revision on June 10, 2022 at 13:51:18 by Anonymous?. See the history of this page for a list of all contributions to it.