lattice.cppm File Reference

Lattice categories — the Form-chain row 4 (#698). More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <limits>
#include <ranges>
#include <tuple>
#include <type_traits>
import dedekind.category:cartesian;

Include dependency graph for lattice.cppm:

Classes
struct	dedekind::category::LatticeBottom< T, Rel >
	Structural witness types for the bottom (initial) and top (terminal) of the lattice over (T, Rel), playing the role of initial / terminal objects of the lattice viewed as a thin category. More...
struct	dedekind::category::LatticeTop< T, Rel >
	The abstract top of the lattice over (T, Rel), dually. More...
struct	dedekind::category::LatticeBottom< T, std::less_equal< T > >
	Canonical specialisation: integral carriers under std::less_equal have bottom = numeric_limits<T>::min(). More...
struct	dedekind::category::LatticeTop< T, std::less_equal< T > >
	Canonical specialisation: integral carriers under std::less_equal have top = numeric_limits<T>::max(). More...
struct	dedekind::category::Meet< A, B >
struct	dedekind::category::Join< A, B >
struct	dedekind::category::predicate_logic< P >
	The logic species a predicate answers in: its own, when it names one (IsSpeciesTaggedArrow), else the species of its answer type, and a composite the species of its last arrow. No type where none applies (a substitution failure, not an error). The lattice nodes over arrows and the combinators and Subobject (:topoi) read this, so a Chain<int> set (answer int, species Chain<int>) conjoins in Chain<int>, and a set pulled back along an arrow (a cylinder, χ ∘ π) answers in the set's species. More...
struct	dedekind::category::predicate_logic< P >
struct	dedekind::category::predicate_logic< Compose< F, G > >
struct	dedekind::category::Meet< A, B >
struct	dedekind::category::Join< A, B >
struct	dedekind::category::Not< A >
struct	dedekind::category::Not< A >
	¬A over an arrow A → Ω is the arrow RFL ∘ A: the codomain's own reflection (generic over any bounded chain Ω: Boole !, Kleene ¬U=U, …). The node stays the literal Not , so is_not_node_v / de_morgan_of / is_complement_pair_v apply unchanged; its set-object reading is structural, downstream in sets. More...
struct	dedekind::category::detail_lattice_nodes::domain_of< T >
	The domain of a term, read off its first leaf. More...
struct	dedekind::category::detail_lattice_nodes::domain_of< Meet< A, B > >
struct	dedekind::category::detail_lattice_nodes::domain_of< Join< A, B > >
struct	dedekind::category::detail_lattice_nodes::domain_of< Not< A > >
struct	dedekind::category::detail_lattice_nodes::same_domain< A, B >
	Two operands on one domain: a lazy trait, read only once both operands qualify, so an operand with no domain is never asked for one. More...
struct	dedekind::category::over_nodes< Leaf, T >
	A property of a term's leaves, lifted over the lattice's nodes: a Meet or Join has it where both operands do and share a domain, a Not where its operand does. One rule for every carrier that lifts a leaf property over the nodes: the opt-in to | and & below, and the set objects of sets (is_set_object). More...
struct	dedekind::category::over_nodes< Leaf, Meet< A, B > >
struct	dedekind::category::over_nodes< Leaf, Join< A, B > >
struct	dedekind::category::over_nodes< Leaf, Not< A > >
struct	dedekind::category::builds_lattice_nodes< T >
	A carrier's opt-in: its predicates' | and & are the lattice's nodes. False by default; a node over two that build does, where they share a domain, by over_nodes, the rule sets' is_set_object follows too. A carrier that opts in keeps the lazy | and &; the set grammar of sets takes the rest, so a type that is both, a Subobject, is the lattice's. This is the lazy form: the node is the result, for intensional and symbolic predicates. A carrier with a normal form reduces at once instead (run lists in :runs, the set grammar in sets); where the lazy and the strict forms meet is not yet uniform (#1138). More...
struct	dedekind::category::detail_lattice_nodes::BuildsNodes
	The opt-in as a leaf property, for over_nodes. More...
struct	dedekind::category::builds_lattice_nodes< Meet< A, B > >
struct	dedekind::category::builds_lattice_nodes< Join< A, B > >
struct	dedekind::category::builds_lattice_nodes< Not< A > >
struct	dedekind::category::MakeMeet
	The pairing factory for the meet (∧, pullback): ⟨-,-⟩ : A×B→Meet. More...
struct	dedekind::category::MakeJoin
	The pairing factory for the join (∨, pushout): ⟨-,-⟩ : A×B→Join. More...
struct	dedekind::category::law_inactive
	Sentinel: a law that does not fire on the given node. More...
struct	dedekind::category::canonical_order
	The default Ord: the carrier's own canonical std::less_equal order (the order bundled with its axioms). A caller whose ∧/∨ mean a different lattice on the same carrier injects that relation as Ord. More...
struct	dedekind::category::is_lattice_bottom_for< X, Ord >
	Is X the registered bottom of the lattice whose order is Ord? More...
struct	dedekind::category::is_lattice_bottom_for< LatticeBottom< T, Rel >, Ord >
struct	dedekind::category::is_lattice_top_for< X, Ord >
	Is X the registered top of the lattice whose order is Ord? More...
struct	dedekind::category::is_lattice_top_for< LatticeTop< T, Rel >, Ord >
struct	dedekind::category::carrier_of< X >
	The carrier type of a reduced term: a value-bearing leaf's ::value type, propagated through Meet / Join composites (a subterm that did not collapse, e.g. Join of two ≤-incomparable elements of a bit-subset lattice), or void when the carrier is unknown (an order-opaque leaf) or inhomogeneous. A composite propagates a carrier only when both children agree on a known one, so a nested mixed-carrier term (at any depth) is void and fails the SameCarrier guard below (fail-closed recursively). More...
struct	dedekind::category::carrier_of< X >
	Carrier of a predicate / subobject leaf. Such a leaf is an arrow χ:Domain→Ω (IsArrow), not a wrapped value, so its carrier is the arrow's Domain. Reading it through IsArrow (the category arrow surface) rather than a bespoke typedef probe ties the reducer into category. The carrier-based gates (SameCarrier, distributivity, complement, De Morgan negation) then apply to set expressions too. An element leaf instead carries ::value, a point 1→T whose carrier is the value's type; the ::value specialisation above handles it. The two spellings extract the carrier from opposite ends of the arrow, so both coexist. More...
struct	dedekind::category::carrier_of< Meet< A, B > >
struct	dedekind::category::carrier_of< Join< A, B > >
struct	dedekind::category::carrier_of< Not< A > >
struct	dedekind::category::codomain_of< X >
	The CODOMAIN Ω of a leaf / term, dual to carrier_of (the domain). A predicate / subobject leaf is an arrow χ:Domain→Ω, so its codomain is Ω (the subobject classifier), read via ::Codomain. A bare value leaf is a truth value, so its codomain is its own type (domain = codomain there, which is why the two-element bool lattice behaves identically under either accessor). Composites propagate the common Ω (fail-closed, exactly like carrier_of). More...
struct	dedekind::category::codomain_of< X >
struct	dedekind::category::codomain_of< Meet< A, B > >
struct	dedekind::category::codomain_of< Join< A, B > >
struct	dedekind::category::codomain_of< Not< A > >
struct	dedekind::category::HeytingExponential< T, std::less_equal< T >, Inf >
	Canonical specialisation: integral carriers under std::less_equal with Inf as the meet. Holds an exponential value value ∈ T; operator()(x) returns Inf(value, x), the lattice meet, which is the eval morphism in a thin Heyting algebra. More...
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. More...
struct	dedekind::category::is_complement< std::logical_not< bool >, bool, std::less_equal< bool >, Sup, Inf >
	Canonical specialisation: std::logical_not<bool> is the complement for the 2-element Boolean lattice over (bool, std::less_equal<bool>, Sup, Inf). Value-level laws hold trivially: true ∧ !true = Inf(true, false) = false = ⊥, and true ∨ !true = Sup(true, false) = true = ⊤. More...

Namespaces
namespace	dedekind::category
namespace	dedekind::category::detail_lattice_nodes

Concepts
concept	dedekind::category::IsLatticeCategory
	A posetal category that is both filtered and cofiltered, with joins and meets given by the algebraic lattice operations.
concept	dedekind::category::IsBoundedLatticeCategory
	A lattice category that has a designated bottom (initial) and top (terminal) element — row 5 of the lattice Form-chain (#698 Slice 4).
concept	dedekind::category::HasLogicSpecies
	The equational laws a lattice concept induces, as compile-time term-reduction rules over the term AST below. Each law is a decomposable, independently-testable part; the assembled reducer (:lattice_term) applies exactly the laws the supplied carrier proves. The richer the carrier's structure (a bounded chain is the sweet spot; bool the optimal witness), the more laws fire and the further a term collapses.
concept	dedekind::category::IsSpeciesTaggedArrow
	An arrow that names its logic species and answers in it: Cod.
concept	dedekind::category::detail_lattice_nodes::BuildNodes
	Two terms whose | and & build nodes: both opted in, on one domain.
concept	dedekind::category::SameCarrier
	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.).
concept	dedekind::category::IsIdempotentLeaf
	T's values are determined by its type, so a type-only lattice law (X∧X=X idempotence, a∧¬a=⊥ complement) collapses soundly on it: two same-type instances are necessarily the same value. A runtime-stateful leaf (say a Singleton holding a value, or a predicate with an expected field) is not idempotent, so those laws must not fire on it, else Meet{S{7},¬S{3}} would wrongly collapse to ⊥. This is the value-safety gate the type-level reducer shares with the value-first :lattice_term reducer (#922). Recursive over Meet / Join / Not through idempotent_leaf_v.
concept	dedekind::category::OrderComparable
	Can A and B be compared in the injected order Ord, at compile time? Both must expose ::value of one carrier type T that is IsPosetal under Ord's resolved relation, and that relation must be default-constructible and constexpr-callable on those values. A registered-but-runtime-only or stateful order therefore fails this guard and the glb/lub collapse stays inactive (fail-closed) rather than hard-erroring.
concept	dedekind::category::IsInvolutiveEndofunctor
	Involutive endofunctor concept — an endomap F : T → T with F² ≅ Id.
concept	dedekind::category::IsHeytingLatticeCategory
	A bounded lattice category whose lattice exponentials are witnessed by :cartesian::IsExponential — row 6 of the lattice Form-chain (#698 Slice 6).
concept	dedekind::category::IsBooleanLatticeCategory
	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).
concept	dedekind::category::IsSubobjectFamilyMember
	Compile-time meeting-point pins (#698 Slice 10) — three structurally distinct carriers at the same Form-chain rows.
concept	dedekind::category::IsSubobjectLattice
	A type S is the carrier of a subobject lattice over S::Domain, with lattice structure induced pointwise from the classifier S::logic_species::Ω.
concept	dedekind::category::IsBooleanSubobjectLattice
	The Form-chain ≤ relation on a subobject lattice is derivable from meet:

Typedefs
template<typename P>
using	dedekind::category::predicate_logic_t = typename predicate_logic<P>::type
template<typename T, typename Ord>
using	dedekind::category::resolved_order_t
	The comparator Ord resolves to for a carrier T: std::less_equal<T> for canonical_order, otherwise Ord itself.
template<typename CA, typename CB>
using	dedekind::category::detail_carrier::common
template<typename X>
using	dedekind::category::carrier_of_t = typename carrier_of<X>::type
template<typename X>
using	dedekind::category::codomain_of_t = typename codomain_of<X>::type

Functions
template<typename A, typename B> requires detail_lattice_nodes::BuildNodes<A, B>
constexpr Join< A, B >	dedekind::category::operator| (A a, B b)
template<typename A, typename B> requires detail_lattice_nodes::BuildNodes<A, B>
constexpr Meet< A, B >	dedekind::category::operator& (A a, B b)
template<typename A, typename B>
constexpr A	dedekind::category::component (const Meet< A, B > &m, At< 1 >)
	π_1: the left-operand accessor of a binary node, returned by const-reference. The operand may itself be a whole set expression (a nested node), and π_1 / π_2 are pure projections. They must not copy the sub-structure. When the operand is a set, π_1(node) is then a bona fide reference to that IsSet (the downstream sets lift relies on this). Still ->convertible_to , so IsProduct is satisfied.
template<typename A, typename B>
constexpr B	dedekind::category::component (const Meet< A, B > &m, At< 2 >)
	π_2: the right-operand accessor of a meet, by const-reference (see π_1).
template<typename A, typename B>
constexpr A	dedekind::category::component (const Join< A, B > &j, At< 1 >)
	π_1: the left-operand accessor of a join, by const-reference (see the meet overload).
template<typename A, typename B>
constexpr B	dedekind::category::component (const Join< A, B > &j, At< 2 >)
	π_2: the right-operand accessor of a join, by const-reference.
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_bounded_law (const RA &a, const RB &b)
	Law induced by a bounded lattice (IsBoundedLatticeCategory): the unit and annihilator. Meet: ⊥∧X=⊥ (annihilator), ⊤∧X=X (unit). Fires only when both operands share a carrier (mixed-carrier ⟹ inactive).
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_bounded_law (const RA &a, const RB &b)
	The join dual: ⊤∨X=⊤ (annihilator), ⊥∨X=X (unit). Likewise fires only when both operands share a carrier.
template<typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::idempotent_law (const RA &a, const RB &)
	Law induced by a (meet/join-)semilattice: idempotence X∧X=X / X∨X=X. Structural: it holds for the lattice operation itself, so it does not depend on the carrier's order. It fires even for order-incomparable opaque leaves. It is gated on idempotent_leaf_v, so a runtime-stateful leaf (two same-type-but-distinct instances) is not collapsed.
template<typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_structural_absorption_law (const RA &a, const RB &b)
	Law induced by a lattice (IsLatticeCategory): structural absorption a∧(a∨b)=a. Structural like idempotence (a lattice axiom needing no order or carrier), so it fires even for order-incomparable opaque leaves; unlike the glb collapse (which needs comparable operands). One level only: nested / associatively-buried occurrences (a∧((a∨b)∨c)) await an associativity-flattening law (tracked on the reducer epic #890). Fails closed on a mixed-carrier term (has_mixed_carrier_v) so it upholds the same recursive fail-closed invariant as carrier_of / the boundary laws; the all-opaque (unknown-carrier) case still fires.
template<typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_structural_absorption_law (const RA &a, const RB &b)
	The join dual: a∨(a∧b)=a. Likewise fails closed on mixed carriers.
template<typename A, typename B, typename Ord>
consteval bool	dedekind::category::order_leq ()
	Is A ≤ B in the injected order Ord? (false when the pair is not compile-time comparable there — the glb/lub law then does not fire.).
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_glb_law (const RA &a, const RB &b)
	Law induced by a lattice's order-meet consistency (RA≤RB ⟺ RA∧RB=RA): for ≤-comparable operands the meet is their glb (the smaller). Note this is not the structural absorption identity a∧(a∨b)=a (which needs no comparison); that is the separate meet_structural_absorption_law. Here only comparable operands collapse.
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_lub_law (const RA &a, const RB &b)
	The join dual: for comparable operands the join is their lub (the larger), RA≤RB ⟹ RA∨RB=RB. (Structural absorption a∨(a∧b)=a is the separate join_structural_absorption_law.).
template<typename X, typename P, typename Q> requires std::copy_constructible<X> && std::copy_constructible<P> && std::copy_constructible<Q>
constexpr auto	dedekind::category::distribute_meet_over (const X &x, const Join< P, Q > &j)
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_distributivity_law (const RA &a, const RB &b)
	Law induced by a distributive lattice: distribute meet over join, X∧(P∨Q) → (X∧P)∨(X∧Q), driving toward a join-of-meets (DNF). One direction only (meet over join, never join over meet), so re-reduction of the result — which the assembler performs — terminates. Gated on both operands sharing a carrier (SameCarrier) whose lattice is distributive under Ord; a chain is gated but pre-empted by the glb collapse, so this fires only on a genuine non-chain distributive lattice.
template<typename B> requires std::copy_constructible<B>
constexpr B	dedekind::category::de_morgan_of (const Not< B > &n)
template<typename P, typename Q> requires std::copy_constructible<P> && std::copy_constructible<Q>
constexpr auto	dedekind::category::de_morgan_of (const Meet< P, Q > &m)
template<typename P, typename Q> requires std::copy_constructible<P> && std::copy_constructible<Q>
constexpr auto	dedekind::category::de_morgan_of (const Join< P, Q > &j)
template<typename Ord, typename RA> requires std::copy_constructible<RA>
constexpr auto	dedekind::category::de_morgan_law (const RA &a)
	Law induced by an involutive De Morgan negation: rewrite ¬(reduced) by involution (¬¬A→A) and De Morgan (¬(A∧B)→¬A∨¬B, ¬(A∨B)→¬A∧¬B), pushing the negation toward the leaves (negation-normal form). Gated on the carrier's lattice carrying such a negation under Ord; a bare ¬leaf is already normal and stays (law_inactive). The driver re-reduces the pushed-down result (termination: ¬ strictly descends).
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_complement_law (const RA &, const RB &)
	Law induced by a complemented lattice: the complement collapse a∧¬a→⊥ (meet) / a∨¬a→⊤ (join). The bottom / top produced is the carrier's registered LatticeBottom / LatticeTop over its resolved order (for sets, that is Ø / 𝔸 once the sets layer registers them). Gated on the carrier being complemented under Ord; else inactive.
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_complement_law (const RA &, const RB &)
	The join dual: a∨¬a→⊤ (excluded middle).
The legs of a node, for @c cata (@c :f_algebra)
The term functor stated once per node: the operands, by reference.
template<typename A, typename B>
constexpr auto	dedekind::category::legs (const Meet< A, B > &m)
template<typename A, typename B>
constexpr auto	dedekind::category::legs (const Join< A, B > &j)
template<typename A>
constexpr auto	dedekind::category::legs (const Not< A > &n)

Variables
template<typename X, typename Ord>
constexpr bool	dedekind::category::is_lattice_bottom_for_v
template<typename X, typename Ord>
constexpr bool	dedekind::category::is_lattice_top_for_v = is_lattice_top_for<X, Ord>::value
template<typename X>
constexpr bool	dedekind::category::has_mixed_carrier_v = false
	Does the term X mix carriers anywhere — either two different known carriers, or a known carrier with an opaque (unknown) one? Only a uniform term fails this: all leaves opaque (the all-unknown case), or all leaves the same known carrier. A known/opaque mix counts as mixed because an opaque leaf carries no evidence it belongs to the known carrier's lattice. The structural laws use this to fail closed on any mixed term while still firing on the all-opaque case. (carrier_of reports void for both all-opaque and mixed, so a per-node is_void mismatch is what distinguishes a known/opaque boundary here.).
template<typename A>
constexpr bool	dedekind::category::has_mixed_carrier_v< Not< A > > = has_mixed_carrier_v<A>
template<typename A, typename B>
constexpr bool	dedekind::category::has_mixed_carrier_v< Meet< A, B > >
template<typename A, typename B>
constexpr bool	dedekind::category::has_mixed_carrier_v< Join< A, B > >
template<typename X>
constexpr bool	dedekind::category::idempotent_leaf_v
	Is X a leaf whose VALUE is determined by its TYPE? Idempotence X∧X=X is sound only for such a leaf. Two same-type instances are then necessarily the same set, so collapsing them is correct. The default is std::is_empty_v<X>, true for a stateless tag or an NTTP-encoded carrier. A carrier with RUNTIME-STATEFUL leaves specialises this to false for them. sets does so for Set<T,L,P> whose predicate P carries a runtime field (e.g. a Point's pivot). The type-based idempotence then does not collapse two distinct-but-same-type values.
template<typename A, typename B>
constexpr bool	dedekind::category::idempotent_leaf_v< Meet< A, B > >
	A compound node is value-determined iff its operands are. So a Meet / Join / Not of value-determined leaves stays collapsible, while one carrying a runtime-stateful leaf does not. This keeps the value-safety gate recursive rather than treating every operand-storing node as stateful (Meet / Join / Not now store their operands, so the bare std::is_empty_v default would report false for all of them).
template<typename A, typename B>
constexpr bool	dedekind::category::idempotent_leaf_v< Join< A, B > >
template<typename A>
constexpr bool	dedekind::category::idempotent_leaf_v< Not< A > > = idempotent_leaf_v<A>
template<typename Elem, typename Node>
constexpr bool	dedekind::category::is_join_containing_v = false
	Is Elem one of the operands of the Join node Node?
template<typename Elem, typename A, typename B>
constexpr bool	dedekind::category::is_join_containing_v< Elem, Join< A, B > >
template<typename Elem, typename Node>
constexpr bool	dedekind::category::is_meet_containing_v = false
	Is Elem one of the operands of the Meet node Node?
template<typename Elem, typename A, typename B>
constexpr bool	dedekind::category::is_meet_containing_v< Elem, Meet< A, B > >
template<typename X>
constexpr bool	dedekind::category::is_join_node_v = false
	Is X a Join node?
template<typename A, typename B>
constexpr bool	dedekind::category::is_join_node_v< Join< A, B > > = true
template<typename T, typename Ord>
constexpr bool	dedekind::category::is_distributive_lattice_for_v
	Is the lattice (carrier T, order Ord) distributive? Keyed to the order like the boundedness markers. The canonical (std::less_equal chain) case derives from the concept gates IsLatticeCategory<T> && IsOrderDistributiveLatticeOperations<T> — so a carrier that is not a lattice under std::less_equal is not licensed to distribute (NB the bare distributive<T>(max{}, min{}) trait is unconditionally true, which would license any carrier — hence the concept gate). A NON-chain distributive lattice (a custom Ord) opts in by specialising this to true (the Jlt assertion — the same posture as the injected total order). A canonical chain is gated distributive but never actually distributes: its joins glb/lub-collapse first.
template<typename X>
constexpr bool	dedekind::category::is_not_node_v = false
	Is X a Not node?
template<typename A>
constexpr bool	dedekind::category::is_not_node_v< Not< A > > = true
template<typename X>
constexpr bool	dedekind::category::is_meet_node_v = false
	Is X a Meet node?
template<typename A, typename B>
constexpr bool	dedekind::category::is_meet_node_v< Meet< A, B > > = true
template<typename T>
constexpr bool	dedekind::category::is_lattice_node_v
	Whether T is one of the nodes, Meet, Join or Not.
template<typename T, typename Ord>
constexpr bool	dedekind::category::is_de_morgan_negation_for_v = false
	Does the lattice (carrier T, order Ord) carry an involutive order-reversing negation (¬¬a=a and the De Morgan laws)? Keyed to the order and opt-in (default false — the Jlt assertion), the same posture as is_distributive_lattice_for_v.
template<>
constexpr bool	dedekind::category::is_de_morgan_negation_for_v< bool, canonical_order > = true
	Canonical bool is a De Morgan (indeed Boolean) algebra: ¬ is std::logical_not, involutive with the De Morgan laws — the production carrier that activates the negation laws (the all-laws-fire oracle).
template<typename T, typename Ord>
constexpr bool	dedekind::category::is_complemented_lattice_for_v = false
	Does the lattice (carrier T, order Ord) carry a genuine complement (a∧¬a=⊥, a∨¬a=⊤), not merely a De Morgan negation? Keyed to the order and opt-in (default false). A complemented lattice is also a De Morgan algebra, so a carrier asserting this should also assert is_de_morgan_negation_for_v.
template<>
constexpr bool	dedekind::category::is_complemented_lattice_for_v< bool, canonical_order >
	Canonical bool is a Boolean (hence complemented) lattice.
template<typename RA, typename RB>
constexpr bool	dedekind::category::is_complement_pair_v
	Are RA and RB a complement pair (RB=¬RA or RA=¬RB)?
template<typename Not, typename T, typename Rel, typename Join, typename Meet>
constexpr bool	dedekind::category::is_complement_v

Detailed Description

Lattice categories — the Form-chain row 4 (#698).

@partition :lattice

lattice__Categorical_Definition

A lattice (in the categorical reading: a thin bicartesian category) is a thin antisymmetric category in which every pair of objects has both a binary product (meet, ∧) and a binary coproduct (join, ∨).

In the order-theoretic encoding the codebase uses across :mereology, :posetal, :thin, :filtered: a lattice over carrier T with relation Rel and topos L assembles

• posetal: thin (preorder) + antisymmetric;
• filtered: every pair has SOME upper bound (directedness);
• cofiltered: every pair has SOME lower bound (codirectedness);
• universality: the upper / lower bounds are unique (join / meet). In the posetal case (antisymmetric) this is automatic — if two least upper bounds a, b exist for a set, then a ≤ b and b ≤ a, hence a = b.

Operationally, the bottom-up algebraic content — join / meet as binary operations satisfying commutativity, associativity, idempotence, and absorption — is named upstream by :posetal::IsOrderLatticeOperations. IsLatticeCategory binds the top-down universal-property reading to the bottom-up algebraic one: every carrier satisfying both presentations is a lattice in the categorical sense.

lattice__Form_Chain

Row 4 of the lattice Form-chain (#698):

IsThinCategory          (row 1, :thin — preorder)
    ↓ + antisymmetry
IsPosetal               (row 2, :posetal — poset)
    ↓ + directedness  ↓ + codirectedness
IsFilteredCategory      (row 3, :filtered — directed poset)
    ↓ + cofiltered + universality
IsLatticeCategory       (row 4, THIS PARTITION)
    ↓ + initial + terminal
IsBoundedLatticeCategory  (row 5, #698 Slice 4 — landed)
    ↓ + exponentials
IsHeytingLatticeCategory  (row 6, #698 Slice 6 — landed)
    ↓ + complement involution
IsBooleanLatticeCategory  (row 7, #698 Slice 7 — THIS SLICE)

Each ↓ + is a faithful inclusion encoded definitionally in the signature, per the project's "faithful specialization in the type signature from day one" posture (#698).

lattice__ETCS_Connection_Sollbruchstelle

Planned downstream connection — not yet structurally landed:

In an ETCS topos (every :etcs::IsSet carrier), the subobject family Sub(S) is automatically a Boolean lattice:

• Axiom 3 (terminal) → initial / terminal in Sub(S) (∅, S).
• Axiom 5 (products) → binary meets (intersection = pullback).
• Axiom 5 + Axiom 7 (Ω) → binary joins (union via classifier).
• Axiom 6 (exponentials) → relative complement (Heyting structure).
• Axiom 7 (classical Ω) → complement involution (Boolean).
• Axiom 10 → direct: Sub(S) is a power-object lattice.

In other words, IsSet implies IsBooleanLatticeCategory<Sub, Boole> once the Form-chain reaches row 7 AND a Sub categorical wrapper exists to host the witness. This connection is a Sollbruchstelle: the partition header names it so future slices (rows 5–7 of the chain + the Sub wrapper + the harmonization of HasAxiom10PowerObjectLattice with the Form-chain) have an unambiguous target.

Until those slices land, the ETCS connection lives at the documentation level only — IsLatticeCategory does not yet require or witness anything about :etcs::IsSet.

lattice__Boolean_Witness

bool with std::less_equal participates: the 2-element poset is also a (Boolean) lattice, and totally-ordered carriers under std::less_equal trivially satisfy directedness and codirectedness (max / min are the join / meet). Pinning bool here anchors the Form-chain at its smallest non-trivial example.

lattice__Omega_First_Pointwise_Lift

Textbook content (#698 Slice 8): the relation between a topos's subobject classifier Ω and the subobject lattices Sub(A) of every ambient A is directional, not symmetric:

Sub(A) ≅ Hom(A, Ω) ≅ Ω^A

gives Sub(A) an automatic lattice structure for every A, inherited pointwise from the lattice structure on Ω. The lattice operations on Sub(A) (meet, join, complement, ≤) correspond pointwise to the lattice operations on Ω (AND, OR, NOT, ≤_Ω) applied to characteristic morphisms χ. Direction is Ω → Sub(A); the reverse doesn't hold without representability.

lattice__Constructive_Collapse

The project commits to intensional-first (lazy predicates over potentially infinite carriers, per Q1 of #698); this admits undecidability as a first-class value via Kleene (Kleene K3). Same Form-chain code, two regimes:

• L = Boole → Ω = bool → Form-chain rows 1–7 → standard set theory falls out as the decidable collapse.
• L = Kleene → Ω = Ternary → Form-chain rows 1–6 (Heyting only — K3 is the smallest non-Boolean Heyting algebra; complement laws fail honestly at Unknown) → the "tricky to decide" escape door.

The Form-chain row a carrier participates in is determined by the carrier's logic_species; the same code witnesses both regimes via parametric polymorphism on L. This is Slice 8's architectural commit: undecidability is architectural (L-parametric), not a corner case (per-branch special-casing).

lattice__Mereology_As_Special_Case

:mereology parthood is a special case of subobject classification: "x is part of y" reads as subset_eq(x, y) on Sub(whole), which is the pointwise lift of ≤_Ω applied to characteristic morphisms. Finite enumerable wholes → Classical → Boolean parthood; infinite / intensional wholes → Kleene → Heyting parthood with honest Unknown at undecidable points. Same Form-chain machinery, one foundation.

lattice__CT_vs_Sets_Vocabulary

Pierce-style stratification: this partition's concept bodies use CT-vocabulary primitives (the classifier Ω, the ambient A, the characteristic morphism χ, free functions meet / join / complement / subset_eq). Default template arguments (Rel = std::less_equal, Join = Sup, ...) are set-theoretic hints — examples, not body content. Operator sugar (<=, &, |, !) lives downstream in :sets as forwarders to the CT primitives.

See also

https://en.wikipedia.org/wiki/Lattice_(order)

https://ncatlab.org/nlab/show/lattice

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note

"Two presentations meet here: the top-down universal-property reading (thin + bicartesian) and the bottom-up algebraic reading (commutative semilattices with absorption). Each side is a witness of the other."

Typedef Documentation

common

template<typename CA, typename CB>

using dedekind::category::detail_carrier::common

Initial value:

 
    std::conditional_t<!std::is_void_v<CA> && std::is_same_v<CA, CB>, CA, void>