Homotopy Type Theory Heyting GCD domain > history (Rev #1)

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

Revision on May 2, 2022 at 18:15:08 by Anonymous?. See the history of this page for a list of all contributions to it.