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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

< GCD domain

Let

category: redirected to nlab
RR be a discrete integral domain, and let us define the type family (−)|(−)(-)\vert(-) as

a|b≔((a=0)→∅)×[∑ c:Ra⋅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 RR can be proven to be a (0,1)-precategory. RR is a discrete GCD domain if (R,|)(R, \vert) is a finitely complete (0,1)-precategory.

See also

Revision on June 13, 2022 at 01:01:17 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (to current)Previous revision (2 more)Current version of pageHide changesHistory (2 revisions)Rollback Source