Showing changes from revision #1 to #2:
Added | Removed | Changed
Let be a Heyting integral domain, and let us define the type family as
The type family is by definition a predicate, and can be proven to be a (0,1)-precategory. is a Heyting GCD domain if is a finitely complete (0,1)-precategory.