Let $R$ be a Heyting integral domain, and let us define the type family $(-)\vert(-)$ as

$a \vert b \coloneqq (a \# 0) \times \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.