Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

~~Let ~~

category: redirected to nlab

$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.

Last revised on June 13, 2022 at 01:01:09. See the history of this page for a list of all contributions to it.