## Definition ## A __Heyting reciprocal ring__ is a [[ring]] $(A, +, -, 0, \cdot, 1)$ with * a [[tight apartness relation]] type family $a # b$ for $a:A$, $b:A$ * a term showing that all endofunctions of $A$ are strongly extensional $$s:\prod_{(f:A \to A)} \prod_{(a:A)} \prod_{(b:A)} (a # b) \to (f(a) # f(b))$$ * an identity showing that every term apart from $0$ has a reciprocal (a two-sided multiplicative inverse) $$r:\prod_{(a:A)} \left( (a # 0) \times \left\Vert \sum_{(b:A)} (a \cdot b = 1) \times (b \cdot a = 1) \right\Vert \right)$$ ## Properties ## Every Heyting reciprocal ring is a [[Heyting division ring]]. ## Examples ## * The [[rational numbers]] are a Heyting reciprocal ring. * Every [[discrete reciprocal ring]] is a Heyting reciprocal ring. * Every [[Heyting division ring]] is a Heyting reciprocal ring. * Every [[Heyting skewfield]] is a Heyting reciprocal ring. ## See also ## * [[ring]] * [[reciprocal ring]]