## Definition ## Let $R$ be a [[discrete integral domain]], and let us define the [[type family]] $(-)\vert(-)$ as $$a \vert b \coloneqq ((a = 0) \to \emptyset) \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 **discrete GCD domain** if $(R, \vert)$ is a [[finitely complete (0,1)-precategory]]. ## See also ## * [[GCD domain]] * [[integral domain]]