## Definition ## Let $R$ be a [[Heyting integral domain]], and let us define the [[type family]] $(-)\vert(-)$ as $$a \vert b \coloneqq \left[\sum_{c:R} a \cdot c = b\right]$$ The type family is by definition a [[predicate]], and $R$ can be proven to be a [[(0,1)-precategory]]. $R$ is a **Heyting GCD domain** if $(R, \vert)$ is a [[finitely complete (0,1)-precategory]]. ## See also ## * [[GCD domain]] * [[integral domain]]