## Definition ## A __Heyting integral domain__ is a [[Heyting domain]] $(A, +, -, 0, \cdot, 1, #)$ with a commutative identity for $\cdot$: $$m_\kappa:\prod_{(a:A)} \prod_{(b:A)} a\cdot b = b\cdot a$$ ## Examples ## * The [[integers]] are a Heyting integral domain. * The [[rational numbers]] are a Heyting integral domain * Every [[discrete integral domain]] is a Heyting integral domain. * Every [[Heyting field]] is a Heyting integral domain. ## See also ## * [[ring]] * [[integral domain]] * [[ordered integral domain]]