dedekind::category::IsBooleanLatticeCategory Concept Reference

A Heyting lattice category whose complement is an involutive endofunctor satisfying the Boolean complement laws — row 7 of the lattice Form-chain (#698 Slice 7). More...

Concept definition

template<typename T, typename Rel std::less_equal<T>, typename Join Sup, typename Meet Inf, typename Not std::logical_not<T>, typename L Boole>
concept dedekind::category::IsBooleanLatticeCategory = 
    IsHeytingLatticeCategory<T, Rel, Join, Meet,
                             L> &&      
    IsInvolutiveEndofunctor<Not, T> &&  
    is_complement_v<Not, T, Rel, Join,
                    Meet>

Detailed Description

A Heyting lattice category whose complement is an involutive endofunctor satisfying the Boolean complement laws — row 7 of the lattice Form-chain (#698 Slice 7).

Faithful inclusion IsBooleanLatticeCategory ⊊ IsHeytingLatticeCategory encoded definitionally per the project's "faithful specialization in the type signature from day one" posture (#698).

lattice__Boolean_Form_Chain_Row_7

Three layered requirements, each a single && term:

• IsHeytingLatticeCategory (structural prerequisite — bounded lattice with exponentials).
• IsInvolutiveEndofunctor<Not, T> (structural: Not : T → T with Not² ≅ Id — Slice 5 machinery).
• is_complement_v<Not, T, Rel, Join, Meet> (semantic opt-in: the complement laws hold for this (@c Not, lattice) pair).

lattice__Boolean_Equivalent_Characterisations

Equivalent textbook readings of "Boolean lattice", any of which the caller can use to recognise the participation:

• A complemented distributive lattice.
• A Heyting algebra in which ¬¬x = x (law of excluded middle).
• A bounded lattice with a unary ¬ satisfying x ∧ ¬x = ⊥ and x ∨ ¬x = ⊤.

This concept threads the third reading definitionally. The first two follow as derived theorems on any carrier participating in the concept (distributivity in a lattice with relative complements is a standard result; double-negation elimination is the registered involutiveness of Not).

lattice__Boolean_Witnesses

• bool under std::less_equal with std::logical_not<bool> — the canonical 2-element Boolean algebra.
• Integral carriers under std::less_equal with std::bit_not are not Boolean lattices (order doesn't match complement); the bitwise Boolean algebra requires a bit-subset Rel (#710).

Template Parameters

T	The Domain (Objects).
Rel	The Relation.
Join	The join operation (default Sup).
Meet	The meet operation (default Inf).
Not	The complement endofunctor (default std::logical_not<T>; fails closed for non-bool unless the carrier registers an alternative pairing).
L	The Logic Species.