Do both operands live in the same, known carrier? The boundary laws require this so a bound of one carrier (e.g. an int ⊤) is never applied as the unit / annihilator of a term whose other operand lives in a different carrier: a mixed-carrier term (⊤ᵢₙₜ ∧ bool-leaf) fails closed. Because the carrier is read via carrier_of, the laws still apply to an arbitrary same-carrier composite subterm (⊤∧X=X even when X is an un-collapsed Meet / Join), not only to leaves. (The glb/lub law forces a shared carrier through OrderComparable; this is its boundary-law counterpart.). More...

Concept definition

template<typename A, typename B>
concept dedekind::category::SameCarrier =  !std::same_as<carrier_of_t<A>, void> &&
                      std::same_as<carrier_of_t<A>, carrier_of_t<B>>

Detailed Description

Do both operands live in the same, known carrier? The boundary laws require this so a bound of one carrier (e.g. an int ⊤) is never applied as the unit / annihilator of a term whose other operand lives in a different carrier: a mixed-carrier term (⊤ᵢₙₜ ∧ bool-leaf) fails closed. Because the carrier is read via carrier_of, the laws still apply to an arbitrary same-carrier composite subterm (⊤∧X=X even when X is an un-collapsed Meet / Join), not only to leaves. (The glb/lub law forces a shared carrier through OrderComparable; this is its boundary-law counterpart.).