Opt-in trait: Not is the complement morphism for the Boolean lattice over (T, Rel, Join, Meet). The trait is the semantic gate for IsBooleanLatticeCategory — the structural side (Heyting + involutiveness of Not) is already enforced by the upstream concepts, but the complement laws. More...

Inheritance diagram for dedekind::category::is_complement< Not, T, Rel, Join, Meet >:

[legend]

Collaboration diagram for dedekind::category::is_complement< Not, T, Rel, Join, Meet >:

[legend]

Detailed Description

template<typename Not, typename T, typename Rel, typename Join, typename Meet>
struct dedekind::category::is_complement< Not, T, Rel, Join, Meet >

Opt-in trait: Not is the complement morphism for the Boolean lattice over (T, Rel, Join, Meet). The trait is the semantic gate for IsBooleanLatticeCategory — the structural side (Heyting + involutiveness of Not) is already enforced by the upstream concepts, but the complement laws.

lattice__Heyting_Canonical_Witnesses

lattice__Boolean_Complement_Trait

x ∧ ¬x = ⊥ , x ∨ ¬x = ⊤

are value-level statements that can't be discharged at type level. Following the is_involutive_v / is_reflexive_v opt-in pattern (#698 Slice 5), the carrier-side registers itself by specialising this trait. Non-canonical pairings (e.g. std::bit_not<int> with std::less_equal<int>) genuinely fail the laws and are excluded by default.

Note: This is a 5-parameter trait, not 6: the logic species L doesn't participate in the complement laws (those are pinned by Rel via lattice_top / lattice_bottom and by Join / Meet directly). Adding L would create spurious specialisation burden for no algebraic content.

The bitwise Boolean algebra on integers (@c int / unsigned with bit-subset Rel, & / | as meet / join, ~ as complement) is a separate canonical witness tracked under #710.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/category/lattice.cppm