Homotopy Type Theory discrete GCD domain > history (Rev #2, changes)

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

Definition

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

a | b ≔ ((a = 0) \to \emptyset) \times [\sum_{c : R} a \cdot c = b]

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.