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


Let RR be a Heyting integral domain, and let us define the type family ()|()(-)\vert(-) as

a|b(a#0)×[ c:Rac=b]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 RR can be proven to be a (0,1)-precategory. RR is a Heyting GCD domain if (R,|)(R, \vert) is a finitely complete (0,1)-precategory.

See also

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