dedekind.relational Module Reference

Concepts
concept	dedekind::relational::IsRelation
	Concept: a set S whose ambient type is std::pair<T1,T2> is a valid binary relation on T1 and T2.
concept	dedekind::relational::IsPairLike
	Pair-like carrier: both coordinates present — the shape every relation (converse, reflexive, symmetric, is_relation) assumes.
concept	dedekind::relational::IsFunctional
concept	dedekind::relational::IsEntire
concept	dedekind::relational::IsFunction
concept	dedekind::relational::IsGraph

Classes
struct	dedekind::relational::FibrePredicate< Rel, T1 >
	The reified fibre of a relation R at a point x: the predicate \(b \mapsto (x,b)\in R\). Named (the sibling of GraphPredicate / PreimagePredicate) so the fibre is stable and inspectable rather than a lambda blackbox (#840). More...
struct	dedekind::relational::SwapPred< P >
	The swapped predicate for converse: \(R^\smile(b,a) = R(a,b)\). More...
struct	dedekind::relational::ComposePred< PR, PS, B >
	The composed predicate for the relative product \(R;S\) over a Boolean intermediate, the ∃-over-the-middle enumerated on {false, true}. More...
struct	dedekind::relational::Intersect< R, S, Meet >
	The point-free composite meet R∩S = Δ† ∘ (R⊗S) ∘ Δ: copy the shared domain, run both legs in parallel, merge their codomain outputs where they agree. The arrow-level (spider) realisation of the relational intersection, whose (Copy,Merge) legs are certified by IsMeetAsRightAdjoint — the same R∩S the extensional operator& above computes over Set<pair>, spelled point-free. More...
struct	dedekind::relational::DiagPred< A >
	The equality-of-coordinates predicate for the diagonal \(\Delta = \{(a,a)\}\). A plain std::equality_comparable check — the diagonal is pure equality, no ordering, so it lives here at the base. More...
struct	dedekind::relational::PairwisePred< Op >
	A binary predicate on A read at the pair ⟨a, b⟩: the other direction of the bridge a set over a product crosses (#1047), so std::less_equal<bool> is a set of pairs. Named, so it carries op and the set inherits every law op has on A (the rules below). More...
struct	dedekind::relational::CoreflexivePred< S >
	The coreflexive predicate for \(\Delta_S = \{(x,x) \mid x \in S\}\) — the diagonal restricted to a unary set S (a partial identity): on the diagonal and in S. Carries S by value so it stays inspectable (no lambda). More...
struct	dedekind::relational::Factor
	A factor of an object: a carrier (a leaf, its sort the column's), or the sum \(X + Y\) of two objects (#1039). A sum lays out a tag column (𝔹: which summand), then the left summand's columns, then the right's; a row reads only the active side, so every column keeps one carrier. More...
struct	dedekind::relational::Object
	An object: a product of factors in normal form, a list. The product is associative with unit 1 (the empty list), so \((A \times B) \times C\) and \(A \times (B \times C)\) are the same object by construction, and >> composes regardless of grouping. Read as a binary tree, (first, rest), where a tree is asked for (kind / operands in Python). The columns are its factors'. More...
struct	dedekind::relational::RelExpr< K, Cs >
	A relation \(A \rightsquigarrow B\) built at run time: a term over relations, its objects dom and cod data, its classifier a reading. More...
struct	dedekind::relational::LawSet< Re, W >
	The relations certified the law W: a datum on the universe of relations, so 𝔸<Re>{} & Total<Re>{} is the set of total relations, membership its χ in K₃ (inferred, or not), and a map or an isomorphism a meet of such sets, nothing stored. Its χ obeys the facts the set is declared: closed under >>, so S(f) ∧ S(g) ≤ S(f >> g); a down-set or an up-set in ⊆; carried by ° to its dagger law. Its complement is never inhabited by inference (¬True, else Unknown): Σ, not Π. More...
struct	dedekind::relational::GraphPredicate< F >
	The membership predicate of a functional graph \(\Gamma_f\): \((a,b)\mapsto b = f(a)\). More...
struct	dedekind::relational::GraphArrow< A, B, P >
	The arrow a function's graph atom names, the converse of graph: a relation A×B | (π_2 == t) certified a function is the arrow a ↦ t(a), t read at a pair whose first coordinate is a. More...
struct	dedekind::relational::PreimagePredicate< F, S >
	The preimage predicate \(a \mapsto f(a)\in S\): the subobject S pulled back along the functional arrow f ( \(\chi_S\circ f\)). More...
struct	dedekind::relational::Fixed< K, C, c, T >
	The arrow that fixes one factor of a pair: \(x \mapsto (c, x)\) (K = 1) or \(x \mapsto (x, c)\) (K = 2). Substitution along it is one case of Shannon's expansion. More...
struct	dedekind::relational::Preimage< F, L >
	\(f^{-1} : \mathrm{Sub}(B, L) \to \mathrm{Sub}(A, L)\), substitution along \(f\): \(b \mapsto \{x \mid f(x) \in b\}\) (preimage, \(\chi_b \circ f\)). Total, a lattice homomorphism, monotone; the right adjoint of Image and the left adjoint of Dual. More...
struct	dedekind::relational::Dual< F, L >
	\(\forall_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the dual image: \(a \mapsto \{y \mid \forall x.\ f(x) = y \Rightarrow x \in a\}\), which is \(\neg\,\exists_f\,\neg\) (De Morgan: the logic is an Ockham algebra), a composite of three arrows on presented objects. The right adjoint of Preimage; monotone, as anti∘co∘anti. More...
struct	dedekind::relational::Image< F, L >
	\(\exists_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the image along \(f : A \to B\): \(a \mapsto f[a] = \{f(x) \mid x \in a\}\). Partial: defined where image_along eliminates the \(\exists\). Monotone; the left adjoint of Preimage. More...

Enumerations
enum class	dedekind::relational::Law : unsigned { Total , Univalent , Injective , Surjective }
	A law of an arrow of Rel, an inclusion: total \(\Delta \le R;R^\circ\), univalent \(R^\circ;R \le \Delta\), injective \(R;R^\circ \le \Delta\), surjective \(\Delta \le R^\circ;R\). Each names the set of the arrows with that law (𝔸<Re> & Total<Re>{}, relational:rows); a map is total and univalent, an isomorphism all four: meets of those sets, with nothing of their own.
enum class	dedekind::relational::Node {   Universe , Comprehension , Meet , Join ,   Not , Converse , Tensor , Compose ,   Sum }
	The nodes of a relational term: its two leaves (the full relation, a comprehension) and the operations of the calculus. RelExpr's Kind (relational:rows), and what the engine reads, free of the representation (a run-time node, a typed predicate).

Typedefs
template<typename T1, typename T2, typename L, typename P>
using	dedekind::relational::Relation = Comprehension<𝔸<std::pair<T1, T2>, L>, P>
	A Relation from A to B is a set of pairs: a subset of A × B.
template<typename T1, typename T2, typename L, typename P>
using	dedekind::relational::SetFunction = Relation<T1, T2, L, P>
	A (set-level) Function is a Relation where each domain element maps to exactly one codomain element. The alias admits the same structure as a Relation; functional totality and single-valuedness are enforced at the call-site via witness elements.
using	dedekind::relational::Laws = dedekind::category::Profile<Law, 4>
	The laws an arrow is certified: one answer in K₃ per law, a profile (category::Profile) over the four. A constexpr value, so the engine is read by the compiler on a typed relation (the traits of :cartesian, below) and by the program over a RelExpr (relational:rows, laws): one engine, two readers.
using	dedekind::relational::Columns = std::vector<std::size_t>
	The sorts of a row, one per column.
template<typename Re>
using	dedekind::relational::Total = LawSet<Re, Law::Total>
template<typename Re>
using	dedekind::relational::Univalent = LawSet<Re, Law::Univalent>
template<typename Re>
using	dedekind::relational::Injective = LawSet<Re, Law::Injective>
template<typename Re>
using	dedekind::relational::Surjective = LawSet<Re, Law::Surjective>
template<typename F>
using	dedekind::relational::Graph
	Graph<F> — the type of graph(f): the Set<pair> relation \(\Gamma_f=\{(a,b)\mid b=f(a)\}\subseteq A\times B\) of F : A→B.

Functions
template<typename T1, typename T2, typename L, typename P, typename C>
constexpr auto	dedekind::relational::dom (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	The declared domain of a relation R ⊆ A×B: the universal set 𝔸 over the first factor — π₁'s codomain.
template<typename T1, typename T2, typename L, typename P, typename C>
constexpr auto	dedekind::relational::cod (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	The declared codomain of a relation R ⊆ A×B: 𝔸, the second factor (π₂'s codomain). Dual to dom.
template<typename T1, typename T2, typename L, typename P, typename C>
constexpr auto	dedekind::relational::apply (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r, const T1 &x)
	Relational application: the image of x under R, the fibre \(\{b \in B \mid (x,b) \in R\}\) as a Set on the codomain.
template<typename T1, typename T2, typename L, typename P, typename C> requires std::invocable<const Comprehension<𝔸<std::pair<T1, T2>, L, C>, P>&, std::pair<T1, T2>>
constexpr auto	dedekind::relational::fibre (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r, const T1 &x)
	fibre(R, x) = the fibre \(\{b \mid (x,b)\in R\}\) as a named comprehension — the lambda-free sibling of apply (#840): the power transpose \(\Lambda R : A \to \mathcal{P}(B)\) read as a first-class subobject.
template<typename T1, typename T2, typename L, typename P, typename C, std::same_as< T1 >... Xs> requires (sizeof...(Xs) >= 1)
constexpr auto	dedekind::relational::fibre (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r, const T1 &x0, const Xs &... xs)
	The relational IMAGE of a finite set of points, given as a pack: \(R[\{x_0,\dots,x_n\}] = \bigcup_i \mathrm{fibre}(R, x_i)\) — the power transpose extended from a point to a finite set, distributing over the join (image preserves unions, the left-adjoint law). Point-free and lambda-free: the structural | union of the named point-fibres, with no enumeration carrier (no array, no ∃). Probes only the given points, so it stays in the point-fibre's complexity class.
template<typename T1, typename T2, typename L, typename P> requires requires(const T2& y) { { y == y } -> dedekind::category::LiftableInto< typename SetFunction<T1, T2, L, P>::logic_species>; }
constexpr auto	dedekind::relational::is_single_valued_at (const SetFunction< T1, T2, L, P > &f, const T1 &x, const T2 &y1, const T2 &y2)
	Point-wise single-valuedness witness for a set-function relation.
template<typename R> requires dedekind::sets::IsSetObject<R> && IsPairLike<typename R::Domain>
constexpr auto	dedekind::relational::converse (const R &r)
	converse(R) — the transpose \(R^\smile \subseteq B \times A\) of a relation \(R \subseteq A \times B\) (Tarski's \(R^\smile\)).
template<typename S>
consteval bool	dedekind::relational::is_relation (const S &)
	is_relation(R) — the bracket-free query: R is a relation, an IsSet whose Domain is a product \(A \times B\).
template<typename A, typename B, typename C, typename L, typename PR, typename PS, typename CR, typename CS> requires std::same_as<B, bool>
constexpr auto	dedekind::relational::operator>> (const Comprehension< 𝔸< std::pair< A, B >, L, CR >, PR > &r, const Comprehension< 𝔸< std::pair< B, C >, L, CS >, PS > &s)
	R >> S — the relative product of two relations over a Boolean intermediate, the ∃-over-the-middle enumerated on {false, true}. A larger intermediate needs the finite-quotient handle (§3.1); there is deliberately no overload, so it is an honest compile error. FIXME(#795): generalise the intermediate beyond bool.
template<typename A, typename B, typename L, typename PR, typename PS, typename C, typename CU>
constexpr auto	dedekind::relational::operator& (const Comprehension< 𝔸< std::pair< A, B >, L, C >, PR > &r, const Comprehension< 𝔸< std::pair< A, B >, L, CU >, PS > &s)
	R & S — the INTERSECTION (meet) of two relations over the same product, dual to the union | (Join): membership is both predicates (RelAnd). The Boolean-lattice ∩ on relations.
template<typename A, typename L = dedekind::category::Boole, typename Op>
constexpr auto	dedekind::relational::relation_of (Op op)
	relation_of<A>(op): the relation \(\{(a, b) \mid op(a, b)\} \subseteq A \times A\) of a binary predicate on A.
template<typename A, typename L = dedekind::category::Boole> requires std::equality_comparable<A>
constexpr auto	dedekind::relational::diag ()
	The DIAGONAL (identity relation) \(\Delta = \{(a,a)\}\) on a carrier A — {π_1==π_2} — the reflexive-closure unit and the 1 of the relation algebra.
template<typename S> requires dedekind::category::IsLSet<S>
constexpr auto	dedekind::relational::diag (const S &s)
	diag(S) — the coreflexive \(\Delta_S = \{(x,x) \mid x \in S\}\), the partial identity on a unary set (Tarski's monotype). Generalizes the full diagonal (diag(𝔸) recovers it) and is the restrictor for a relative product's endpoints, so a set pre-image is \(\mathrm{dom}(R \mathbin{;} \mathrm{diag}(S))\) without leaving the point-free surface.
template<typename R> requires dedekind::sets::IsSetObject<R> && IsPairLike<typename R::Domain> && std::same_as<typename R::Domain::first_type, typename R::Domain::second_type>
constexpr auto	dedekind::relational::reflexive (const R &r)
	reflexive(R) = R | Δ — the smallest reflexive relation containing an endorelation R (add the self-loops). P is constrained to a genuine pair-predicate (invocable on a carrier pair \(\langle A,A \rangle\)) so a mis-typed R fails at the call, not deep inside the union.
template<typename R> requires dedekind::sets::IsSetObject<R> && IsPairLike<typename R::Domain> && std::same_as<typename R::Domain::first_type, typename R::Domain::second_type>
constexpr auto	dedekind::relational::symmetric (const R &r)
	symmetric(R) = R | R° — the smallest symmetric relation containing R (add the reversed edges; R° is the converse).
constexpr auto	dedekind::relational::conv (const auto &r)
constexpr auto	dedekind::relational::dagger (const auto &r)
constexpr auto	dedekind::relational::refl (const auto &r)
constexpr auto	dedekind::relational::sym (const auto &r)
constexpr auto	dedekind::relational::Δ (const auto &s)
constexpr bool	dedekind::relational::closed_under (Law w, Node n)
	Closure: the arrows with the law w form a sub-algebra under n. Each of the four is closed under ; and ⊗. The + of this calculus is the sum of two tables, \(1 \to A + B\) (not the direct sum of arrows \(1 + 1 \to A + B\)): one input, both outputs, so it keeps totality, surjectivity and injectivity but not univalence.
constexpr bool	dedekind::relational::is_up_set (Law w)
	Variance in the inclusion order: total and surjective are up-sets (R ≤ S and R total ⇒ S total), univalent and injective down-sets (S univalent ⇒ R univalent).
constexpr Law	dedekind::relational::dagger (Law w)
	The dagger's action: ° carries total to surjective and univalent to injective, an involution on the laws.
constexpr dedekind::category::Ternary	dedekind::relational::infer (Law w, Node n, dedekind::category::Ternary a, dedekind::category::Ternary b=dedekind::category::Ternary::Unknown)
	The engine, one for every law and every representation: a node's answer in K₃ from the law's facts and its legs' answers a, b. Where the set is closed under the node, both legs; a down-set holds f & g when it holds f or g (f & g ≤ f), an up-set holds f | g likewise; ° is answered by the operand at the dagger law (a, looked up by the caller); ~ by no fact. True where inferred, Unknown where no fact applies, never False: the facts certify, they do not refute (sound, not complete). So for a closed set S, S(f) ∧ S(g) ≤ S(f >> g): a law of the sets' χ, tested in rows_test.
constexpr Laws	dedekind::relational::laws_from (bool total, bool univalent, bool injective, bool surjective)
	Declared answers, read off four witnesses.
constexpr Laws	dedekind::relational::node_laws (Node n, const Laws &a, const Laws &b={})
	The engine at a node, law by law: the legs' answers in, the node's out; ° reads its operand at the dagger law.
template<dedekind::sets::IsSetObject S, typename Pred> requires std::invocable<const std::decay_t<Pred>&, const typename S::Domain&> && requires(std::invoke_result_t<const std::decay_t<Pred>&, const typename S::Domain&> v) { { dedekind::category::lift_logic<typename S::logic_species>(v) } -> std::same_as<typename S::logic_species::Ω>; }
constexpr auto	dedekind::relational::select (const S &s, Pred pred)
	Selection (σ): filter elements of a set by an additional predicate.
template<dedekind::sets::IsSetObject A, dedekind::sets::IsSetObject B> requires std::same_as<typename A::Domain, typename B::Domain>
constexpr auto	dedekind::relational::set_union (const A &a, const B &b)
	Union (∪): elements belonging to at least one of two same-typed sets.
template<dedekind::sets::IsSetObject A, dedekind::sets::IsSetObject B> requires std::same_as<typename A::Domain, typename B::Domain>
constexpr auto	dedekind::relational::set_difference (const A &a, const B &b)
	Difference (∖): elements of A that are absent from B.
template<typename A, typename B> requires dedekind::category::IsLSet<std::remove_cvref_t<A>> && dedekind::category::IsLSet<std::remove_cvref_t<B>> && requires(const A& a, const B& b) { a & ~b; }
constexpr auto	dedekind::relational::operator- (const A &a, const B &b)
	operator- : the set-difference operator, \(A \setminus B = A \cap \sim\! B\).
template<dedekind::sets::IsSetObject A, dedekind::sets::IsSetObject B> requires std::same_as<typename A::Domain, typename B::Domain>
constexpr auto	dedekind::relational::set_intersection (const A &a, const B &b)
	Intersection (∩): elements common to both sets.
template<dedekind::sets::IsSetObject R1, dedekind::sets::IsSetObject R2> requires IsPairLike<typename R1::Domain> && IsPairLike<typename R2::Domain> && std::same_as<typename R1::Domain::second_type, typename R2::Domain::first_type> && std::same_as<typename R1::logic_species, typename R2::logic_species>
constexpr auto	dedekind::relational::natural_join (const R1 &r1, const R2 &r2)
	Natural join (⋈): compose two binary relations on a shared middle type.
constexpr auto	dedekind::relational::σ (auto &&... a)
constexpr auto	dedekind::relational::join (auto &&... a)
constexpr Columns	dedekind::relational::columns (const Object &o)
	The columns of an object: a fold over its factors, per factor a leaf's sort; a sum's tag, then its left summand's columns, then its right's.
constexpr Object	dedekind::relational::sum (const Object &x, const Object &y, std::size_t tag)
	The object \(X + Y\): one sum factor, its tag column of sort tag (the 𝔹 carrier's).
constexpr Object	dedekind::relational::operator* (const Object &a, const Object &b)
	The product \(A \times B\): the factors side by side (the normal form of an associative product).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator& (const RelExpr< K, Cs... > &r, const dedekind::sets::Pred< K > &p)
	R & p: the former, the meet with the subobject p classifies (#826), every slot, constant and operator of p checked in its column's sort now.
template<typename K, typename... Cs>
RelExpr< K, Cs... >	dedekind::relational::operator| (const RelExpr< K, Cs... > &, const dedekind::sets::Pred< K > &)=delete
	R | p: refused; the filter is R & p (#826).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator& (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	R & S and R | S between the same objects: the lattice's nodes.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator| (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator~ (const RelExpr< K, Cs... > &a)
	~R: the complement.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::converse (const RelExpr< K, Cs... > &a)
	R°: the converse, \(B \rightsquigarrow A\), the dagger.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator* (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	R * S: the tensor \(R \otimes S : A \times C \rightsquigarrow B \times D\). Two universes make the product universe (the universe over a product is the product of the universes).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator>> (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	R >> S: Kleisli composition, \(R;S : A \rightsquigarrow C\) for \(R : A \rightsquigarrow B\) and \(S : B \rightsquigarrow C\), the ∃ over the whole middle object \(B\).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::table (const RelExpr< K, Cs... > &r)
	\(A \rightsquigarrow B\) read as the table \(1 \rightsquigarrow A \times B\): every factor moved to the codomain. Rel is compact closed, \(A \times B \rightsquigarrow C \cong A \rightsquigarrow B \times C\), so the rows are the same; only >>, * and converse see where the factors sit. Whole factors move: a sum's columns stay together.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::arrow (const RelExpr< K, Cs... > &r)
	A relation read as the arrow of all its factors but the last (the Function[A, …, B] convention): \(1 \rightsquigarrow A_1 \times \dots \times A_n\) as \(A_1 \times \dots \times A_{n-1} \rightsquigarrow A_n\). The same compact-closed iso as table, the other way.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::sum (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	\(A + B\): the sum of two tables (sets), a table over the object \(X + Y\), its χ the copairing \([\chi_A, \chi_B]\) on the tag.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::diag (const Object &obj)
	η: the identity \(\Delta_A = \{(x, x)\}\), the unit of >>.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::copy (const Object &obj)
	Copy: \(A \rightsquigarrow A \times A\), \(x \mapsto (x, x)\), the comonoid of the Frobenius structure.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::merge (const Object &obj)
	Merge: \(A \times A \rightsquigarrow A\), the converse of copy.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::proj (const Object &obj, const std::vector< unsigned > &keep)
	The structural projection \(\pi : A \rightsquigarrow A[keep]\), the columns keep (1-based) of the object in that order.
template<typename K, typename... Cs>
constexpr dedekind::sets::Pred< K >	dedekind::relational::predicate_of (const RelExpr< K, Cs... > &r)
	The predicate of a relation on the columns of its domain then its codomain, π_1 … π_n: a reading of the term. A universe ⊤ (over a sum, the rows that encode a point: encodes); a former its predicate on its base's; the lattice nodes their connectives (a complement the negation normal form, ∃ and ∀ swapped); a converse its base's with the two objects' columns exchanged; a tensor the conjunction, the columns arranged domain, domain, codomain, codomain; a composite the ∃ over every column of the middle object (the monad's μ), outermost first. A quantifier binds the next slot past the columns, so a leg's own bound slots are renumbered with its columns and never captured.
template<typename K, typename... Cs>
constexpr dedekind::category::Ternary	dedekind::relational::verdict (const RelExpr< K, Cs... > &r, const typename RelExpr< K, Cs... >::Point &row)
	χ at a row of the columns, in K₃: the predicate reading with every quantifier an atom defines eliminated first (the fusion law), the rest searched within the relation's budget. The one χ: Python binds this.
template<typename K, typename... Cs>
constexpr Laws	dedekind::relational::laws (const RelExpr< K, Cs... > &r)
	The laws of a relation, inferred: a fold over the term reading the engine (infer, :dyadic) at each node, the leaves certified by their shape (detail_rows::predicate_laws), at the relation's own split of its columns into domain and codomain. True where a rule infers the law, Unknown where none does; the normal form may still decide the inclusion (algebra, canonical).
template<typename K, typename... Cs>
constexpr std::optional< std::vector< dedekind::sets::Term< K > > >	dedekind::relational::function_terms (const RelExpr< K, Cs... > &r, const dedekind::sets::Pred< K > &p)
	The value of a relation certified a map, as terms: per codomain column the term over the domain columns that defines it in p, when every codomain column is so defined and nothing else is asked (what makes a leaf total and univalent by its shape); nothing otherwise. What ap(R, x) evaluates.
template<typename F> requires dedekind::category::IsArrow<F> && std::equality_comparable<typename std::remove_cvref_t<F>::Codomain>
constexpr Graph< std::remove_cvref_t< F > >	dedekind::relational::graph (F f)
	graph(f) — the graph of a function f : A → B as the Set of pairs \(\{\,(a,b) \mid b = f(a)\,\} \subseteq A\times B\).
template<typename R> requires dedekind::sets::IsGraphAtom<std::remove_cvref_t< decltype(std::declval<const R&>().predicate)>> && IsFunctional<R> && IsEntire<R>
constexpr auto	dedekind::relational::arrow_of (const R &r)
	arrow_of(R): the arrow of a relation certified a function (a graph atom, functional and entire), the converse of graph: graph(arrow_of(R)) is R and arrow_of(graph(f)) is f.
template<typename U, typename F>
constexpr F	dedekind::relational::arrow_of (const Comprehension< U, GraphPredicate< F > > &g)
	arrow_of(graph(f)): the graph keeps its arrow, so it is f itself.
template<typename F, typename G> requires IsFunctional<Graph<F>> && IsFunctional<Graph<G>> && std::same_as<typename F::Codomain, typename G::Domain>
constexpr auto	dedekind::relational::operator>> (const Graph< F > &r, const Graph< G > &s)
	Relative product of two functional relations (graphs), over any intermediate: \(\Gamma_f\,;\,\Gamma_g = \Gamma_{f;g}\).
template<typename F, typename S> requires dedekind::category::IsArrow<F> && (!dedekind::category::IsLSet<std::remove_cvref_t<F>>) && requires(const S& s, const typename std::remove_cvref_t<F>::Codomain& b) { typename std::remove_cvref_t<S>::logic_species; { s(b) } -> std::same_as<typename std::remove_cvref_t<S>::logic_species::Ω>; }
constexpr auto	dedekind::relational::preimage (F f, S s)
	preimage(f, S) = \(\{\,a \mid f(a)\in S\,\}\) — the subobject S ⊆ B pulled back along f : A → B, i.e. S's classifier composed with f ( \(\chi_S\circ f\); every mono is a pullback of true, so a preimage IS such a pullback).
template<std::size_t K, typename X, typename Y, dedekind::sets::IsSetObject S>
constexpr auto	dedekind::relational::image_along (const dedekind::category::Injection< K, X, Y > &, const S &s)
	\(\exists_\iota\) along an injection: the sum's pushforward.
template<typename X, dedekind::sets::IsSetObject S>
constexpr auto	dedekind::relational::image_along (const dedekind::category::Copy< X > &, const S &s)
	\(\exists_\Delta\) along the diagonal: the coreflexive \(\Delta_S = \{(x, x) \mid x \in S\}\), diag.
template<dedekind::category::IsPairProjection< 1 > F, dedekind::sets::IsSetObject R> requires dedekind::category::IsFiniteChain< typename dedekind::category::Dom<F>::second_type> && dedekind::category::HasNNOStep< typename dedekind::category::Dom<F>::second_type>
constexpr auto	dedekind::relational::image_along (const F &, const R &r)
	\(\exists_{\pi_1}\), the second factor a finite chain: Shannon.
template<dedekind::category::IsPairProjection< 2 > F, dedekind::sets::IsSetObject R> requires dedekind::category::IsFiniteChain< typename dedekind::category::Dom<F>::first_type> && dedekind::category::HasNNOStep< typename dedekind::category::Dom<F>::first_type>
constexpr auto	dedekind::relational::image_along (const F &, const R &r)
	\(\exists_{\pi_2}\), the first factor a finite chain: Shannon.
template<typename R, typename F, std::ranges::input_range DomRange, std::ranges::input_range CodRange> requires dedekind::category::IsArrow<F> && std::same_as<std::ranges::range_value_t<DomRange>, dedekind::category::Dom<F>> && std::same_as<std::ranges::range_value_t<CodRange>, dedekind::category::Cod<F>>
constexpr auto	dedekind::relational::is_graph_of (const R &r, F f, const DomRange &dom, const CodRange &cod)
	is_graph_of(r, f, dom) — the finite witness that a relation r is the graph of the arrow f, by pointwise agreement with graph(f) over the enumerable domain dom.

Variables
constexpr std::array< Law, 4 >	dedekind::relational::every_law
template<typename R>
constexpr Laws	dedekind::relational::laws_of_v
	The engine read for a typed relation: its four laws as the :cartesian traits answer them, declared on a leaf or inferred on a node (the readers in the category namespace below).

Files
file	src/main/modules/dedekind/relational/relational.cppm
	dedekind.relational — a first-class module for relations, popped out of :sets: Codd's relational model, Tarski's calculus of relations, and graphs (of arrows, binary relations).
file	src/main/modules/dedekind/relational/dyadic.cppm
	Tarski's calculus of (dyadic) relations: converse R°, the relative product R;S, union/meet, the diagonal Δ, over Set<pair> — the BASE partition of dedekind.relational.
file	src/main/modules/dedekind/relational/graph.cppm
	The graph of a function as a relation: the analytic arrow f and its set of pairs are one object. A graph is a dyadic (binary) relation (functional \(R\subseteq A\times B\) for \(f:A\to B\); an endorelation only when \(A=B\)), so it lives with the relations (dedekind.relational), not in :sets.
file	src/main/modules/dedekind/relational/rows.cppm
	Relations built at run time as terms: arrows \(A \rightsquigarrow B\) between products of carriers, their objects data (#1037).
file	src/main/modules/dedekind/relational/tables.cppm
	Codd's relational model — the query algebra over typed, intensional Sets and Relations (σ select, π-elided, ⋈ join, ∪, ∖, ∩).