The Form-chain ≤ relation on a subobject lattice is derivable from meet: More...

Concept definition

template<typename S>
concept dedekind::category::IsBooleanSubobjectLattice = 
    IsSubobjectLattice<S> && std::same_as<typename S::logic_species, Boole>

Detailed Description

The Form-chain ≤ relation on a subobject lattice is derivable from meet:

lattice__IsSubobjectLattice_Order_Derivability

a ≤ b ⟺ meet(a, b) = a ⟺ join(a, b) = b

This is a standard textbook equivalence (Birkhoff, "Lattice Theory", §1.4). Hence IsSubobjectLattice's body does not require a separate subset_eq / operator<= clause — the row-1 (thin) inclusion content is recoverable from the row-3 (filtered) lattice ops. Carriers exposing a direct operator<= or free subset_eq do so as set-side sugar (the Pierce-style stratification named in Slice 8's Sollbruchstelle text), not as a CT-vocabulary primitive of this concept.

A subobject lattice over a classical classifier — the Boolean refinement that closes the L-parametric gap (#698 Slice 9 review pass).

Mechanises the user's downstream intuition: parametrising a set carrier with Boole should automatically participate in the Boolean lattice surface; parametrising with Kleene should not. The previous parallel-track architecture left this documentation-only ("easy to forget" per the review thread); this concept makes it type-checked.

lattice__IsBooleanSubobjectLattice_Justification

In topos-theoretic terms: a topos with classical subobject classifier (Ω = bool) has Boolean Sub(A) for every ambient A. This is automatic — no semantic opt-in required at the family level beyond the logic_species commitment. Diaconescu's theorem (1975) further says the full Axiom of Choice would propagate Boolean-ness in the reverse direction, but the converse direction we use here (classical Ω ⟹ Boolean Sub(A)) is uncontroversial.

The concept is therefore just IsSubobjectLattice + L = Boole — no extra structural laws beyond what IsSubobjectLattice already checks. Kleene / Heyting carriers fail closed because their logic_species ≠ Boole.

Template Parameters

S	The subobject carrier.